1 /-
2 Copyright (c) 2019 Sébastien Gouëzel. All rights reserved.
3 Released under Apache 2.0 license as described in the file LICENSE.
4 Author: Sébastien Gouëzel
5 -/
6
7 import topology.metric_space.closeds set_theory.cardinal topology.metric_space.gromov_hausdorff_realized
src └───────────────────────────┘ └─────────────────┘ └─────────────────────────────────────────────┘
8 topology.metric_space.completion
src └──────────────────────────────┘
9
10 /-!
11 # Gromov-Hausdorff distance
12
13 This file defines the Gromov-Hausdorff distance on the space of nonempty compact metric spaces
14 up to isometry.
15
16 We introduce the space of all nonempty compact metric spaces, up to isometry,
17 called `GH_space`, and endow it with a metric space structure. The distance,
18 known as the Gromov-Hausdorff distance, is defined as follows: given two
19 nonempty compact spaces `X` and `Y`, their distance is the minimum Hausdorff distance
20 between all possible isometric embeddings of `X` and `Y` in all metric spaces.
21 To define properly the Gromov-Hausdorff space, we consider the non-empty
22 compact subsets of `ℓ^∞(ℝ)` up to isometry, which is a well-defined type,
23 and define the distance as the infimum of the Hausdorff distance over all
24 embeddings in `ℓ^∞(ℝ)`. We prove that this coincides with the previous description,
25 as all separable metric spaces embed isometrically into `ℓ^∞(ℝ)`, through an
26 embedding called the Kuratowski embedding.
27 To prove that we have a distance, we should show that if spaces can be coupled
28 to be arbitrarily close, then they are isometric. More generally, the Gromov-Hausdorff
29 distance is realized, i.e., there is a coupling for which the Hausdorff distance
30 is exactly the Gromov-Hausdorff distance. This follows from a compactness
31 argument, essentially following from Arzela-Ascoli.
32
33 ## Main results
34
35 We prove the most important properties of the Gromov-Hausdorff space: it is a polish space,
36 i.e., it is complete and second countable. We also prove the Gromov compactness criterion.
37
38 -/
39
40 noncomputable theory
41 open_locale classical topological_space
42 universes u v w
43
44 open classical lattice set function topological_space filter metric quotient
45 open bounded_continuous_function nat Kuratowski_embedding
46 open sum (inl inr)
47 set_option class.instance_max_depth 50
doc └──────────────────────┘
48
49 local attribute [instance] metric_space_sum
id └──────────────┘
src └──────────────┘
typ └──────────────┘
doc └──────────────┘
50
51
52 namespace Gromov_Hausdorff
53
54 section GH_space
55 /- In this section, we define the Gromov-Hausdorff space, denoted `GH_space` as the quotient
56 of nonempty compact subsets of `ℓ^∞(ℝ)` by identifying isometric sets.
57 Using the Kuratwoski embedding, we get a canonical map `to_GH_space` mapping any nonempty
58 compact type to `GH_space`. -/
59
60 /-- Equivalence relation identifying two nonempty compact sets which are isometric -/
61 private definition isometry_rel : nonempty_compacts ℓ_infty_ℝ → nonempty_compacts ℓ_infty_ℝ → Prop :=
id └───────────────┘ └───────┘ └───────────────┘ └───────┘
src └───────────────┘ └───────┘ └───────────────┘ └───────┘
typ └───────────────┘ └───────┘ └───────────────┘ └───────┘
doc └───────────────┘ └───────┘ └───────────────┘ └───────┘
62 λx y, nonempty (x.val ≃ᵢ y.val)
id ┴ ┴ └──────┘ ┴└──┘ └┘ ┴└──┘
src └──────┘ └──┘ └┘ └──┘
typ ┴ ┴ └──────┘ ┴└──┘ └┘ ┴└──┘
doc └┘
63
64 /-- This is indeed an equivalence relation -/
65 private lemma is_equivalence_isometry_rel : equivalence isometry_rel :=
id └─────────┘ └──────────┘
src └─────────┘ └──────────┘
typ └─────────┘ └──────────┘
doc └──────────┘
66 ⟨λx, ⟨isometric.refl _⟩, λx y ⟨e⟩, ⟨e.symm⟩, λ x y z ⟨e⟩ ⟨f⟩, ⟨e.trans f⟩⟩
id ┴ └────────────┘ ┴ ┴ ┴┴ └───┘ ┴ ┴ ┴ ┴┴ ┴┴ └────┘
src └────────────┘ └───┘ └────┘
typ ┴ └────────────┘ ┴ ┴ ┴┴ └───┘ ┴ ┴ ┴ ┴┴ ┴┴ └────┘
doc └────────────┘ └───┘ └────┘
67
68 /-- setoid instance identifying two isometric nonempty compact subspaces of ℓ^∞(ℝ) -/
69 instance isometry_rel.setoid : setoid (nonempty_compacts ℓ_infty_ℝ) :=
id └────┘ └───────────────┘ └───────┘
src └────┘ └───────────────┘ └───────┘
typ └────┘ └───────────────┘ └───────┘
doc └───────────────┘ └───────┘
70 setoid.mk isometry_rel is_equivalence_isometry_rel
id └───────┘ └──────────┘ └─────────────────────────┘
src └───────┘ └──────────┘ └─────────────────────────┘
typ └───────┘ └──────────┘ └─────────────────────────┘
doc └──────────┘ └─────────────────────────┘
71
72 /-- The Gromov-Hausdorff space -/
73 definition GH_space : Type := quotient (isometry_rel.setoid)
id └──────┘ └─────────────────┘
src └──────┘ └─────────────────┘
typ └──────┘ └─────────────────┘
doc └─────────────────┘
74
75 /-- Map any nonempty compact type to `GH_space` -/
76 definition to_GH_space (α : Type u) [metric_space α] [compact_space α] [nonempty α] : GH_space :=
id └──────────┘ ┴ └───────────┘ ┴ └──────┘ ┴ └──────┘
src └──────────┘ └───────────┘ └──────┘ └──────┘
typ └──────────┘ ┴ └───────────┘ ┴ └──────┘ ┴ └──────┘
doc └──────────┘ └───────────┘ └──────┘
77 ⟦nonempty_compacts.Kuratowski_embedding α⟧
id ┴└────────────────────────────────────┘ ┴┴
src ┴└────────────────────────────────────┘ ┴
typ ┴└────────────────────────────────────┘ ┴┴
doc └────────────────────────────────────┘
78
79 instance : inhabited GH_space := ⟨quot.mk _ ⟨{0}, by simp⟩⟩
id └───────┘ └──────┘ └─────┘ ┴
src └───────┘ └──────┘ ┴ └──┘
typ └───────┘ └──────┘ └─────┘ ┴ └──┘
doc └──────┘ └──┘
txt └──┘
par └──┘
st └───┘
80
81 /-- A metric space representative of any abstract point in `GH_space` -/
82 definition GH_space.rep (p : GH_space) : Type := (quot.out p).val
id └──────┘ └──────┘ ┴ └─┘
src └──────┘ └──────┘ └─┘
typ └──────┘ └──────┘ ┴ └─┘
doc └──────┘ └──────┘
83
84 lemma eq_to_GH_space_iff {α : Type u} [metric_space α] [compact_space α] [nonempty α] {p : nonempty_compacts ℓ_infty_ℝ} :
id └──────────┘ ┴ └───────────┘ ┴ └──────┘ ┴ └───────────────┘ └───────┘
src └──────────┘ └───────────┘ └──────┘ └───────────────┘ └───────┘
typ └──────────┘ ┴ └───────────┘ ┴ └──────┘ ┴ └───────────────┘ └───────┘
doc └──────────┘ └───────────┘ └───────────────┘ └───────┘
85 ⟦p⟧ = to_GH_space α ↔ ∃Ψ : α → ℓ_infty_ℝ, isometry Ψ ∧ range Ψ = p.val :=
id ┴┴┴ ┴ └─────────┘ ┴ ┴ ┴ ┴ ┴ └───────┘┴ └──────┘ ┴ ┴ └───┘ ┴ ┴ ┴└──┘
src ┴ ┴ ┴ └─────────┘ ┴ ┴ └───────┘┴ └──────┘ ┴ └───┘ ┴ └──┘
typ ┴┴┴ ┴ └─────────┘ ┴ ┴ ┴ ┴ ┴ └───────┘┴ └──────┘ ┴ ┴ └───┘ ┴ ┴ ┴└──┘
doc └─────────┘ └───────┘ └──────┘ └───┘
86 begin
st └─────
87 simp only [to_GH_space, quotient.eq],
id └─────────┘ └─────────┘
src └─────────┘└─────────┘└┘└─────────┘┴
typ └─────────┘└─────────┘└┘└─────────┘┴
doc └─────────┘└─────────┘└┘ ┴
txt └─────────┘ └┘ ┴
par └─────────┘ └┘ ┴
pid ┴└──┘└┘ └┘ ┴
st ─────────────────────────────────────┘└─
88 split,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ──────┘└─
89 { assume h,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid └──────┘
st ───┘└──────┘└─
90 rcases setoid.symm h with ⟨e⟩,
id └─────────┘ ┴
src └─────┘└─────────┘┴ └───────┘
typ └─────┘└─────────┘┴┴└───────┘
doc └─────┘ ┴ └───────┘
txt └─────┘ ┴ └───────┘
par └─────┘ ┴ └───────┘
pid ┴ ┴ └───────┘
st ────────────────────────────────┘└─
91 have f := (Kuratowski_embedding.isometry α).isometric_on_range.trans e,
id └───────────────────────────┘ ┴ ┴
src └────────┘ └───────────────────────────┘┴ └─────────────────────────┘
typ └────────┘ └───────────────────────────┘┴┴└─────────────────────────┘┴
doc └────────┘ └───────────────────────────┘┴ └─────────────────────────┘
txt └────────┘ ┴ └─────────────────────────┘
par └────────┘ ┴ └─────────────────────────┘
pid └────┘┴└─┘ ┴ └─────────────────────────┘
st ─────────────────────────────────────────────────────────────────────────┘└─
92 use λx, f x,
id ┴
src └──┘ └─┘ ┴
typ └──┘ └─┘┴┴
doc └──┘ └─┘ ┴
txt └──┘ └─┘ ┴
par └──┘ └─┘ ┴
pid ┴ └─┘ ┴
st ──────────────┘└─
93 split,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ────────┘└─
94 { apply isometry_subtype_val.comp f.isometry },
id └───────────────────────┘ └────────┘
src └────┘└───────────────────────┘┴└────────┘┴
typ └────┘└───────────────────────┘┴└────────┘┴
doc └────┘└───────────────────────┘┴ ┴
txt └────┘ ┴ ┴
par └────┘ ┴ ┴
pid ┴ ┴ ┴
st ─────┘└─────────────────────────────────────────┘└┘└
95 { rw [range_comp, f.range_coe, set.image_univ, set.range_coe_subtype] } },
id └────────┘ └────────────┘ └───────────────────┘
src └──┘└────────┘└┘ └┘└────────────┘└┘└───────────────────┘└┘
typ └──┘└────────┘└┘└─────────┘└┘└────────────┘└┘└───────────────────┘└┘
doc └──┘ └┘ └┘ └┘ └┘
txt └──┘ └┘ └┘ └┘ └┘
par └──┘ └┘ └┘ └┘ └┘
pid └┘ └┘ └┘ └┘ ┴┴
st ───────────────────┘└───────────┘└──────────────┘└─────────────────────┘┴┴└──┘└
96 { rintros ⟨Ψ, ⟨isomΨ, rangeΨ⟩⟩,
src └──────────────────────────┘
typ └──────────────────────────┘
doc └──────────────────────────┘
txt └──────────────────────────┘
par └──────────────────────────┘
pid └───────────────────┘
st ───────────────────────────────┘└─
97 have f := ((Kuratowski_embedding.isometry α).isometric_on_range.symm.trans
id └───────────────────────────┘ ┴
src └────────┘ └───────────────────────────┘┴ └───────────────────────────────
typ └────────┘ └───────────────────────────┘┴┴└───────────────────────────────
doc └────────┘ └───────────────────────────┘┴ └───────────────────────────────
txt └────────┘ ┴ └───────────────────────────────
par └────────┘ ┴ └───────────────────────────────
pid └────┘┴└─┘ ┴ └───────────────────────────────
st ───────────────────────────────────────────────────────────────────────────────
98 isomΨ.isometric_on_range).symm,
id └──────────────────────┘
src ──────────────┘└──────────────────────┘└────┘
typ ──────────────┘└──────────────────────┘└────┘
doc ──────────────┘└──────────────────────┘└────┘
txt ──────────────┘ └────┘
par ──────────────┘ └────┘
pid ──────────────┘ └───┘┴
st ────────────────────────────────────────────┘└─
99 have E : (range Ψ ≃ᵢ (nonempty_compacts.Kuratowski_embedding α).val) = (p.val ≃ᵢ range (Kuratowski_embedding α)),
id ┴ └┘ └────────────────────────────────────┘ ┴ └───┘ └───┘ └──────────────────┘ ┴
src └───────┘ ┴ ┴└┘┴ └────────────────────────────────────┘┴ └─────┘┴┴ └───┘┴ ┴└───┘┴ └──────────────────┘┴ └┘
typ └───────┘ ┴┴┴└┘┴ └────────────────────────────────────┘┴ └─────┘┴┴ └───┘┴ ┴└───┘┴ └──────────────────┘┴┴└┘
doc └───────┘ ┴ ┴└┘┴ └────────────────────────────────────┘┴ └─────┘ ┴ ┴ ┴└───┘┴ └──────────────────┘┴ └┘
txt └───────┘ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ └┘
par └───────┘ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ └┘
pid └────┘└─┘ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ └┘
st ───────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
100 by { dunfold nonempty_compacts.Kuratowski_embedding, rw [rangeΨ]; refl },
id └────┘
src └────────────────────────────────────────────┘ └──┘ ┴ └───┘
typ └────────────────────────────────────────────┘ └──┘└────┘┴ └───┘
doc └────────────────────────────────────────────┘ └──┘ ┴ └───┘
txt └────────────────────────────────────────────┘ └──┘ ┴ └───┘
par └────────────────────────────────────────────┘ └──┘ ┴ └───┘
pid └─────────────────────────────────────┘ └┘ ┴ ┴
st ┴└─────────────────────────────────────────────┘└──────────┘┴└─────┘└┘└
101 have g := cast E f,
id └──┘ ┴ ┴
src └────────┘└──┘┴ ┴
typ └────────┘└──┘┴┴┴┴
doc └────────┘ ┴ ┴
txt └────────┘ ┴ ┴
par └────────┘ ┴ ┴
pid └────┘┴└─┘ ┴ ┴
st ─────────────────────┘└─
102 exact ⟨g⟩ }
id ┴
src └────┘ └┘
typ └────┘ ┴└┘
doc └────┘ └┘
txt └────┘ └┘
par └────┘ └┘
pid ┴ ┴┴
st ─────────────┘└─
103 end
st ──┘
104
105 lemma eq_to_GH_space {p : nonempty_compacts ℓ_infty_ℝ} : ⟦p⟧ = to_GH_space p.val :=
id └───────────────┘ └───────┘ ┴┴┴ ┴ └─────────┘ ┴└──┘
src └───────────────┘ └───────┘ ┴ ┴ ┴ └─────────┘ └──┘
typ └───────────────┘ └───────┘ ┴┴┴ ┴ └─────────┘ ┴└──┘
doc └───────────────┘ └───────┘ └─────────┘
106 begin
st └─────
107 refine eq_to_GH_space_iff.2 ⟨((λx, x) : p.val → ℓ_infty_ℝ), _, subtype.val_range⟩,
id └────────────────┘ └───┘ └───────┘ └───────────────┘
src └─────┘└────────────────┘└─┘ └─┘ └──┘└───┘┴ ┴└───────┘└────┘└───────────────┘┴
typ └─────┘└────────────────┘└─┘ └─┘ └──┘└───┘┴ ┴└───────┘└────┘└───────────────┘┴
doc └─────┘ └─┘ └─┘ └──┘ ┴ ┴└───────┘└────┘ ┴
txt └─────┘ └─┘ └─┘ └──┘ ┴ ┴ └────┘ ┴
par └─────┘ └─┘ └─┘ └──┘ ┴ ┴ └────┘ ┴
pid ┴ └─┘ └─┘ └──┘ ┴ ┴ └────┘ ┴
st ─────────────────────────────────────────────────────────────────────────────────┘└─
108 apply isometry_subtype_val
id └──────────────────┘
src └────┘└──────────────────┘┴
typ └────┘└──────────────────┘┴
doc └────┘└──────────────────┘┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ───────────────────────────┘
109 end
st └─┘
110
111 section
112 local attribute [reducible] GH_space.rep
id └──────────┘
src └──────────┘
typ └──────────┘
doc └───────┘ └──────────┘
113
114 instance rep_GH_space_metric_space {p : GH_space} : metric_space (p.rep) :=
id └──────┘ └──────────┘ ┴└──┘
src └──────┘ └──────────┘ └──┘
typ └──────┘ └──────────┘ ┴└──┘
doc └──────┘ └──────────┘ └──┘
115 by apply_instance
src └──────────────
typ └──────────────
doc └──────────────
txt └──────────────
par └──────────────
pid └
st └───────────────
116
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
117 instance rep_GH_space_compact_space {p : GH_space} : compact_space (p.rep) :=
id └──────┘ └───────────┘ ┴└──┘
src └──────┘ └───────────┘ └──┘
typ └──────┘ └───────────┘ ┴└──┘
doc └──────┘ └───────────┘ └──┘
118 by apply_instance
src └──────────────
typ └──────────────
doc └──────────────
txt └──────────────
par └──────────────
pid └
st └───────────────
119
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
120 instance rep_GH_space_nonempty {p : GH_space} : nonempty (p.rep) :=
id └──────┘ └──────┘ ┴└──┘
src └──────┘ └──────┘ └──┘
typ └──────┘ └──────┘ ┴└──┘
doc └──────┘ └──┘
121 by apply_instance
src └─────────────┘
typ └─────────────┘
doc └─────────────┘
txt └─────────────┘
par └─────────────┘
pid ┴
st └──────────────┘
122 end
123
124 lemma GH_space.to_GH_space_rep (p : GH_space) : to_GH_space (p.rep) = p :=
id └──────┘ └─────────┘ ┴└──┘ ┴ ┴
src └──────┘ └─────────┘ └──┘ ┴
typ └──────┘ └─────────┘ ┴└──┘ ┴ ┴
doc └──────┘ └─────────┘ └──┘
125 begin
st └─────
126 change to_GH_space (quot.out p).val = p,
id └─────────┘ └──────┘ ┴ ┴
src └─────┘└─────────┘┴ └──────┘┴ └────┘┴┴
typ └─────┘└─────────┘┴ └──────┘┴ └────┘┴┴┴
doc └─────┘└─────────┘┴ └──────┘┴ └────┘ ┴
txt └─────┘ ┴ ┴ └────┘ ┴
par └─────┘ ┴ ┴ └────┘ ┴
pid ┴ ┴ ┴ └────┘ ┴
st ────────────────────────────────────────┘└─
127 rw ← eq_to_GH_space,
id └────────────┘
src └───┘└────────────┘
typ └───┘└────────────┘
doc └───┘
txt └───┘
par └───┘
pid └─┘
st ────────────────────┘└─
128 exact quot.out_eq p
id └─────────┘ ┴
src └────┘└─────────┘┴ ┴
typ └────┘└─────────┘┴┴┴
doc └────┘ ┴ ┴
txt └────┘ ┴ ┴
par └────┘ ┴ ┴
pid ┴ ┴ ┴
st ─────────────────────┘
129 end
st └─┘
130
131 /-- Two nonempty compact spaces have the same image in `GH_space` if and only if they are isometric -/
132 lemma to_GH_space_eq_to_GH_space_iff_isometric {α : Type u} [metric_space α] [compact_space α] [nonempty α]
id └──────────┘ ┴ └───────────┘ ┴ └──────┘ ┴
src └──────────┘ └───────────┘ └──────┘
typ └──────────┘ ┴ └───────────┘ ┴ └──────┘ ┴
doc └──────────┘ └───────────┘
133 {β : Type u} [metric_space β] [compact_space β] [nonempty β] :
id └──────────┘ ┴ └───────────┘ ┴ └──────┘ ┴
src └──────────┘ └───────────┘ └──────┘
typ └──────────┘ ┴ └───────────┘ ┴ └──────┘ ┴
doc └──────────┘ └───────────┘
134 to_GH_space α = to_GH_space β ↔ nonempty (α ≃ᵢ β) :=
id └─────────┘ ┴ ┴ └─────────┘ ┴ ┴ └──────┘ ┴ └┘ ┴
src └─────────┘ ┴ └─────────┘ ┴ └──────┘ └┘
typ └─────────┘ ┴ ┴ └─────────┘ ┴ ┴ └──────┘ ┴ └┘ ┴
doc └─────────┘ └─────────┘ └┘
135 ⟨begin
st └─────
136 simp only [to_GH_space, quotient.eq],
id └─────────┘ └─────────┘
src └─────────┘└─────────┘└┘└─────────┘┴
typ └─────────┘└─────────┘└┘└─────────┘┴
doc └─────────┘└─────────┘└┘ ┴
txt └─────────┘ └┘ ┴
par └─────────┘ └┘ ┴
pid ┴└──┘└┘ └┘ ┴
st ─────────────────────────────────────┘└─
137 assume h,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid └──────┘
st ─────────┘└─
138 rcases h with e,
id ┴
src └─────┘ └─────┘
typ └─────┘┴└─────┘
doc └─────┘ └─────┘
txt └─────┘ └─────┘
par └─────┘ └─────┘
pid ┴ └─────┘
st ────────────────┘└─
139 have I : ((nonempty_compacts.Kuratowski_embedding α).val ≃ᵢ (nonempty_compacts.Kuratowski_embedding β).val)
id └┘ └────────────────────────────────────┘
src └───────┘ ┴ └────┘└┘┴ └────────────────────────────────────┘┴ └──────
typ └───────┘ ┴ └────┘└┘┴ └────────────────────────────────────┘┴ └──────
doc └───────┘ ┴ └────┘└┘┴ └────────────────────────────────────┘┴ └──────
txt └───────┘ ┴ └────┘ ┴ ┴ └──────
par └───────┘ ┴ └────┘ ┴ ┴ └──────
pid └────┘└─┘ ┴ └────┘ ┴ ┴ └──────
st ──────────────────────────────────────────────────────────────────────────────────────────────────────────────
140 = ((range (Kuratowski_embedding α)) ≃ᵢ (range (Kuratowski_embedding β))),
id ┴ ┴ └───┘ └──────────────────┘ ┴
src ─────────┘┴┴ ┴ ┴ └─┘ ┴ └───┘┴ └──────────────────┘┴ └─┘
typ ─────────┘┴┴ ┴ ┴┴└─┘ ┴ └───┘┴ └──────────────────┘┴┴└─┘
doc ─────────┘ ┴ ┴ ┴ └─┘ ┴ └───┘┴ └──────────────────┘┴ └─┘
txt ─────────┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └─┘
par ─────────┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └─┘
pid ─────────┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └─┘
st ─────────────────────────────────────────────────────────────────────────────────┘
141 by { dunfold nonempty_compacts.Kuratowski_embedding, refl },
src └────────────────────────────────────────────┘ └───┘
typ └────────────────────────────────────────────┘ └───┘
doc └────────────────────────────────────────────┘ └───┘
txt └────────────────────────────────────────────┘ └───┘
par └────────────────────────────────────────────┘ └───┘
pid └─────────────────────────────────────┘ ┴
st ┴└─────────────────────────────────────────────┘└─────┘└┘└
142 have e' := cast I e,
id └──┘ ┴ ┴
src └─────────┘└──┘┴ ┴
typ └─────────┘└──┘┴┴┴┴
doc └─────────┘ ┴ ┴
txt └─────────┘ ┴ ┴
par └─────────┘ ┴ ┴
pid └─────┘┴└─┘ ┴ ┴
st ────────────────────┘└─
143 have f := (Kuratowski_embedding.isometry α).isometric_on_range,
id └───────────────────────────┘ ┴
src └────────┘ └───────────────────────────┘┴ └──────────────────┘
typ └────────┘ └───────────────────────────┘┴┴└──────────────────┘
doc └────────┘ └───────────────────────────┘┴ └──────────────────┘
txt └────────┘ ┴ └──────────────────┘
par └────────┘ ┴ └──────────────────┘
pid └────┘┴└─┘ ┴ └─────────────────┘┴
st ───────────────────────────────────────────────────────────────┘└─
144 have g := (Kuratowski_embedding.isometry β).isometric_on_range.symm,
id └───────────────────────────┘ ┴
src └────────┘ └───────────────────────────┘┴ └───────────────────────┘
typ └────────┘ └───────────────────────────┘┴┴└───────────────────────┘
doc └────────┘ └───────────────────────────┘┴ └───────────────────────┘
txt └────────┘ ┴ └───────────────────────┘
par └────────┘ ┴ └───────────────────────┘
pid └────┘┴└─┘ ┴ └──────────────────────┘┴
st ────────────────────────────────────────────────────────────────────┘└─
145 have h := (f.trans e').trans g,
id └─────┘ └┘ ┴
src └────────┘ └─────┘┴ └──────┘
typ └────────┘ └─────┘┴└┘└──────┘┴
doc └────────┘ └─────┘┴ └──────┘
txt └────────┘ ┴ └──────┘
par └────────┘ ┴ └──────┘
pid └────┘┴└─┘ ┴ └──────┘
st ───────────────────────────────┘└─
146 exact ⟨h⟩
id ┴
src └────┘ └┘
typ └────┘ ┴└┘
doc └────┘ └┘
txt └────┘ └┘
par └────┘ └┘
pid ┴ ┴┴
st ───────────┘
147 end,
st └─┘
148 begin
st └─────
149 rintros ⟨e⟩,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └──┘
st ────────────┘└─
150 simp only [to_GH_space, quotient.eq],
id └─────────┘ └─────────┘
src └─────────┘└─────────┘└┘└─────────┘┴
typ └─────────┘└─────────┘└┘└─────────┘┴
doc └─────────┘└─────────┘└┘ ┴
txt └─────────┘ └┘ ┴
par └─────────┘ └┘ ┴
pid ┴└──┘└┘ └┘ ┴
st ─────────────────────────────────────┘└─
151 have f := (Kuratowski_embedding.isometry α).isometric_on_range.symm,
id └───────────────────────────┘ ┴
src └────────┘ └───────────────────────────┘┴ └───────────────────────┘
typ └────────┘ └───────────────────────────┘┴┴└───────────────────────┘
doc └────────┘ └───────────────────────────┘┴ └───────────────────────┘
txt └────────┘ ┴ └───────────────────────┘
par └────────┘ ┴ └───────────────────────┘
pid └────┘┴└─┘ ┴ └──────────────────────┘┴
st ────────────────────────────────────────────────────────────────────┘└─
152 have g := (Kuratowski_embedding.isometry β).isometric_on_range,
id └───────────────────────────┘ ┴
src └────────┘ └───────────────────────────┘┴ └──────────────────┘
typ └────────┘ └───────────────────────────┘┴┴└──────────────────┘
doc └────────┘ └───────────────────────────┘┴ └──────────────────┘
txt └────────┘ ┴ └──────────────────┘
par └────────┘ ┴ └──────────────────┘
pid └────┘┴└─┘ ┴ └─────────────────┘┴
st ───────────────────────────────────────────────────────────────┘└─
153 have h := (f.trans e).trans g,
id └─────┘ ┴ ┴
src └────────┘ └─────┘┴ └──────┘
typ └────────┘ └─────┘┴┴└──────┘┴
doc └────────┘ └─────┘┴ └──────┘
txt └────────┘ ┴ └──────┘
par └────────┘ ┴ └──────┘
pid └────┘┴└─┘ ┴ └──────┘
st ──────────────────────────────┘└─
154 have I : ((range (Kuratowski_embedding α)) ≃ᵢ (range (Kuratowski_embedding β))) =
id └───┘ └──────────────────┘
src └───────┘ ┴ ┴ └─┘ ┴ └───┘┴ └──────────────────┘┴ └──┘ └
typ └───────┘ ┴ ┴ └─┘ ┴ └───┘┴ └──────────────────┘┴ └──┘ └
doc └───────┘ ┴ ┴ └─┘ ┴ └───┘┴ └──────────────────┘┴ └──┘ └
txt └───────┘ ┴ ┴ └─┘ ┴ ┴ ┴ └──┘ └
par └───────┘ ┴ ┴ └─┘ ┴ ┴ ┴ └──┘ └
pid └────┘└─┘ ┴ ┴ └─┘ ┴ ┴ ┴ └──┘ └
st ────────────────────────────────────────────────────────────────────────────────────
155 ((nonempty_compacts.Kuratowski_embedding α).val ≃ᵢ (nonempty_compacts.Kuratowski_embedding β).val),
id ┴ └────────────────────────────────────┘ ┴
src ───┘ ┴ └────┘ ┴ └────────────────────────────────────┘┴ └────┘
typ ───┘ ┴┴└────┘ ┴ └────────────────────────────────────┘┴┴└────┘
doc ───┘ ┴ └────┘ ┴ └────────────────────────────────────┘┴ └────┘
txt ───┘ ┴ └────┘ ┴ ┴ └────┘
par ───┘ ┴ └────┘ ┴ ┴ └────┘
pid ───┘ ┴ └────┘ ┴ ┴ └────┘
st ─────────────────────────────────────────────────────────────────────────────────────────────────────┘
156 by { dunfold nonempty_compacts.Kuratowski_embedding, refl },
src └────────────────────────────────────────────┘ └───┘
typ └────────────────────────────────────────────┘ └───┘
doc └────────────────────────────────────────────┘ └───┘
txt └────────────────────────────────────────────┘ └───┘
par └────────────────────────────────────────────┘ └───┘
pid └─────────────────────────────────────┘ ┴
st ┴└─────────────────────────────────────────────┘└─────┘└┘└
157 have h' := cast I h,
id └──┘ ┴ ┴
src └─────────┘└──┘┴ ┴
typ └─────────┘└──┘┴┴┴┴
doc └─────────┘ ┴ ┴
txt └─────────┘ ┴ ┴
par └─────────┘ ┴ ┴
pid └─────┘┴└─┘ ┴ ┴
st ────────────────────┘└─
158 exact ⟨h'⟩
id └┘
src └────┘ └┘
typ └────┘ └┘└┘
doc └────┘ └┘
txt └────┘ └┘
par └────┘ └┘
pid ┴ ┴┴
st ────────────┘
159 end⟩
st └─┘
160
161 /-- Distance on `GH_space`: the distance between two nonempty compact spaces is the infimum
162 Hausdorff distance between isometric copies of the two spaces in a metric space. For the definition,
163 we only consider embeddings in `ℓ^∞(ℝ)`, but we will prove below that it works for all spaces. -/
164 instance : has_dist (GH_space) :=
id └──────┘ └──────┘
src └──────┘ └──────┘
typ └──────┘ └──────┘
doc └──────┘ └──────┘
165 { dist := λx y, Inf ((λp : nonempty_compacts ℓ_infty_ℝ × nonempty_compacts ℓ_infty_ℝ, Hausdorff_dist p.1.val p.2.val) ''
id ┴ ┴ └─┘ └───────────────┘ └───────┘ ┴ └───────────────┘ └───────┘ └────────────┘ ┴┴ └─┘ ┴┴ └─┘ └┘
src └─┘ └───────────────┘ └───────┘ ┴ └───────────────┘ └───────┘ └────────────┘ ┴ └─┘ ┴ └─┘ └┘
typ ┴ ┴ └─┘ └───────────────┘ └───────┘ ┴ └───────────────┘ └───────┘ └────────────┘ ┴┴ └─┘ ┴┴ └─┘ └┘
doc └─┘ └───────────────┘ └───────┘ └───────────────┘ └───────┘ └────────────┘
166 (set.prod {a | ⟦a⟧ = x} {b | ⟦b⟧ = y})) }
id └──────┘ ┴┴ ┴┴┴ ┴ ┴ ┴┴ ┴┴┴ ┴ ┴
src └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ └──────┘ ┴┴ ┴┴┴ ┴ ┴ ┴┴ ┴┴┴ ┴ ┴
doc └──────┘
167
168 /-- The Gromov-Hausdorff distance between two nonempty compact metric spaces, equal by definition to
169 the distance of the equivalence classes of these spaces in the Gromov-Hausdorff space. -/
170 def GH_dist (α : Type u) (β : Type v) [metric_space α] [nonempty α] [compact_space α]
id └──────────┘ ┴ └──────┘ ┴ └───────────┘ ┴
src └──────────┘ └──────┘ └───────────┘
typ └──────────┘ ┴ └──────┘ ┴ └───────────┘ ┴
doc └──────────┘ └───────────┘
171 [metric_space β] [nonempty β] [compact_space β] : ℝ := dist (to_GH_space α) (to_GH_space β)
id └──────────┘ ┴ └──────┘ ┴ └───────────┘ ┴ ┴ └──┘ └─────────┘ ┴ └─────────┘ ┴
src └──────────┘ └──────┘ └───────────┘ ┴ └──┘ └─────────┘ └─────────┘
typ └──────────┘ ┴ └──────┘ ┴ └───────────┘ ┴ ┴ └──┘ └─────────┘ ┴ └─────────┘ ┴
doc └──────────┘ └───────────┘ └─────────┘ └─────────┘
172
173 lemma dist_GH_dist (p q : GH_space) : dist p q = GH_dist (p.rep) (q.rep) :=
id └──────┘ └──┘ ┴ ┴ ┴ └─────┘ ┴└──┘ ┴└──┘
src └──────┘ └──┘ ┴ └─────┘ └──┘ └──┘
typ └──────┘ └──┘ ┴ ┴ ┴ └─────┘ ┴└──┘ ┴└──┘
doc └──────┘ └─────┘ └──┘ └──┘
174 by rw [GH_dist, p.to_GH_space_rep, q.to_GH_space_rep]
id └─────┘
src └──┘└─────┘└┘ └┘ └─
typ └──┘└─────┘└┘└───────────────┘└┘└───────────────┘└─
doc └──┘└─────┘└┘ └┘ └─
txt └──┘ └┘ └┘ └─
par └──┘ └┘ └┘ └─
pid └┘ └┘ └┘ ┴└
st └──────────┘└─────────────────┘└─────────────────┘┴└
175
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
176 /-- The Gromov-Hausdorff distance between two spaces is bounded by the Hausdorff distance
177 of isometric copies of the spaces, in any metric space. -/
178 theorem GH_dist_le_Hausdorff_dist {α : Type u} [metric_space α] [compact_space α] [nonempty α]
id └──────────┘ ┴ └───────────┘ ┴ └──────┘ ┴
src └──────────┘ └───────────┘ └──────┘
typ └──────────┘ ┴ └───────────┘ ┴ └──────┘ ┴
doc └──────────┘ └───────────┘
179 {β : Type v} [metric_space β] [compact_space β] [nonempty β]
id └──────────┘ ┴ └───────────┘ ┴ └──────┘ ┴
src └──────────┘ └───────────┘ └──────┘
typ └──────────┘ ┴ └───────────┘ ┴ └──────┘ ┴
doc └──────────┘ └───────────┘
180 {γ : Type w} [metric_space γ] {Φ : α → γ} {Ψ : β → γ} (ha : isometry Φ) (hb : isometry Ψ) :
id └──────────┘ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴ └──────┘ ┴
src └──────────┘ └──────┘ └──────┘
typ └──────────┘ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴ └──────┘ ┴
doc └──────────┘ └──────┘ └──────┘
181 GH_dist α β ≤ Hausdorff_dist (range Φ) (range Ψ) :=
id └─────┘ ┴ ┴ ┴ └────────────┘ └───┘ ┴ └───┘ ┴
src └─────┘ ┴ └────────────┘ └───┘ └───┘
typ └─────┘ ┴ ┴ ┴ └────────────┘ └───┘ ┴ └───┘ ┴
doc └─────┘ └────────────┘ └───┘ └───┘
182 begin
st └─────
183 /- For the proof, we want to embed `γ` in `ℓ^∞(ℝ)`, to say that the Hausdorff distance is realized
st ─────────────────────────────────────────────────────────────────────────────────────────────────────
184 in `ℓ^∞(ℝ)` and therefore bounded below by the Gromov-Hausdorff-distance. However, `γ` is not
st ────────────────────────────────────────────────────────────────────────────────────────────────
185 separable in general. We restrict to the union of the images of `α` and `β` in `γ`, which is
st ───────────────────────────────────────────────────────────────────────────────────────────────
186 separable and therefore embeddable in `ℓ^∞(ℝ)`. -/
st ─────────────────────────────────────────────────────
187 rcases exists_mem_of_nonempty α with ⟨xα, _⟩,
id └────────────────────┘ ┴
src └─────┘└────────────────────┘┴ └───────────┘
typ └─────┘└────────────────────┘┴┴└───────────┘
doc └─────┘ ┴ └───────────┘
txt └─────┘ ┴ └───────────┘
par └─────┘ ┴ └───────────┘
pid ┴ ┴ └───────────┘
st ─────────────────────────────────────────────┘└─
188 letI : inhabited α := ⟨xα⟩,
id └───────┘ ┴ └┘
src └─────┘└───────┘┴ └──┘ ┴
typ └─────┘└───────┘┴┴└──┘ └┘┴
doc └─────┘ ┴ └──┘ ┴
txt └─────┘ ┴ └──┘ ┴
par └─────┘ ┴ └──┘ ┴
pid ┴└┘ ┴ └──┘ ┴
st ───────────────────────────┘└─
189 letI : inhabited β := classical.inhabited_of_nonempty (by assumption),
id └───────┘ ┴ └─────────────────────────────┘
src └─────┘└───────┘┴ └──┘└─────────────────────────────┘┴ ┴└────────┘┴
typ └─────┘└───────┘┴┴└──┘└─────────────────────────────┘┴ ┴└────────┘┴
doc └─────┘ ┴ └──┘ ┴ ┴└────────┘┴
txt └─────┘ ┴ └──┘ ┴ ┴└────────┘┴
par └─────┘ ┴ └──┘ ┴ ┴└────────┘┴
pid ┴└┘ ┴ └──┘ ┴ └──────────┘
st ──────────────────────────────────────────────────────────┘└─────────┘┴└─
190 let s : set γ := (range Φ) ∪ (range Ψ),
id └─┘ ┴ ┴ ┴ └───┘ ┴
src └──────┘└─┘┴ └──┘ ┴ └┘┴┴ └───┘┴ ┴
typ └──────┘└─┘┴┴└──┘ ┴┴└┘┴┴ └───┘┴┴┴
doc └──────┘ ┴ └──┘ ┴ └┘ ┴ └───┘┴ ┴
txt └──────┘ ┴ └──┘ ┴ └┘ ┴ ┴ ┴
par └──────┘ ┴ └──┘ ┴ └┘ ┴ ┴ ┴
pid └───┘└─┘ ┴ └──┘ ┴ └┘ ┴ ┴ ┴
st ───────────────────────────────────────┘└─
191 let Φ' : α → subtype s := λy, ⟨Φ y, mem_union_left _ (mem_range_self _)⟩,
id ┴ └─────┘ ┴ ┴ └────────────┘ └────────────┘
src └───────┘ ┴ ┴└─────┘┴ └──┘ └─┘ ┴ └┘└────────────┘└─┘ └────────────┘└──┘
typ └───────┘┴┴ ┴└─────┘┴┴└──┘ └─┘ ┴┴ └┘└────────────┘└─┘ └────────────┘└──┘
doc └───────┘ ┴ ┴ ┴ └──┘ └─┘ ┴ └┘ └─┘ └──┘
txt └───────┘ ┴ ┴ ┴ └──┘ └─┘ ┴ └┘ └─┘ └──┘
par └───────┘ ┴ ┴ ┴ └──┘ └─┘ ┴ └┘ └─┘ └──┘
pid └────┘└─┘ ┴ ┴ ┴ └──┘ └─┘ ┴ └┘ └─┘ └──┘
st ─────────────────────────────────────────────────────────────────────────┘└─
192 let Ψ' : β → subtype s := λy, ⟨Ψ y, mem_union_right _ (mem_range_self _)⟩,
id ┴ └─────┘ ┴ ┴ └─────────────┘ └────────────┘
src └───────┘ ┴ ┴└─────┘┴ └──┘ └─┘ ┴ └┘└─────────────┘└─┘ └────────────┘└──┘
typ └───────┘┴┴ ┴└─────┘┴┴└──┘ └─┘ ┴┴ └┘└─────────────┘└─┘ └────────────┘└──┘
doc └───────┘ ┴ ┴ ┴ └──┘ └─┘ ┴ └┘ └─┘ └──┘
txt └───────┘ ┴ ┴ ┴ └──┘ └─┘ ┴ └┘ └─┘ └──┘
par └───────┘ ┴ ┴ ┴ └──┘ └─┘ ┴ └┘ └─┘ └──┘
pid └────┘└─┘ ┴ ┴ ┴ └──┘ └─┘ ┴ └┘ └─┘ └──┘
st ──────────────────────────────────────────────────────────────────────────┘└─
193 have IΦ' : isometry Φ' := λx y, ha x y,
id └──────┘ └┘ └┘
src └─────────┘└──────┘┴ └──┘ └───┘ ┴ ┴
typ └─────────┘└──────┘┴└┘└──┘ └───┘└┘┴ ┴
doc └─────────┘└──────┘┴ └──┘ └───┘ ┴ ┴
txt └─────────┘ ┴ └──┘ └───┘ ┴ ┴
par └─────────┘ ┴ └──┘ └───┘ ┴ ┴
pid └──────┘└─┘ ┴ └──┘ └───┘ ┴ ┴
st ───────────────────────────────────────┘└─
194 have IΨ' : isometry Ψ' := λx y, hb x y,
id └──────┘ └┘ └┘
src └─────────┘└──────┘┴ └──┘ └───┘ ┴ ┴
typ └─────────┘└──────┘┴└┘└──┘ └───┘└┘┴ ┴
doc └─────────┘└──────┘┴ └──┘ └───┘ ┴ ┴
txt └─────────┘ ┴ └──┘ └───┘ ┴ ┴
par └─────────┘ ┴ └──┘ └───┘ ┴ ┴
pid └──────┘└─┘ ┴ └──┘ └───┘ ┴ ┴
st ───────────────────────────────────────┘└─
195 have : compact s, from (compact_range ha.continuous).union (compact_range hb.continuous),
id └─────┘ ┴ └───────────┘ └───────────┘ └───────────┘
src └─────┘└─────┘┴ └───┘ ┴└───────────┘└──────┘ └───────────┘┴└───────────┘┴
typ └─────┘└─────┘┴┴ └───┘ ┴└───────────┘└──────┘ └───────────┘┴└───────────┘┴
doc └─────┘└─────┘┴ └───┘ ┴└───────────┘└──────┘ ┴└───────────┘┴
txt └─────┘ ┴ └───┘ ┴ └──────┘ ┴ ┴
par └─────┘ ┴ └───┘ ┴ └──────┘ ┴ ┴
pid └───┘└┘ ┴ └───┘ ┴ └──────┘ ┴ ┴
st ─────────────────┘└──────────────────────────────────────────────────────────────────────┘└─
196 letI : metric_space (subtype s) := by apply_instance,
id └──────────┘ └─────┘ ┴
src └─────┘└──────────┘┴ └─────┘┴ └───┘ ┴└────────────┘
typ └─────┘└──────────┘┴ └─────┘┴┴└───┘ ┴└────────────┘
doc └─────┘└──────────┘┴ ┴ └───┘ ┴└────────────┘
txt └─────┘ ┴ ┴ └───┘ ┴└────────────┘
par └─────┘ ┴ ┴ └───┘ ┴└────────────┘
pid ┴└┘ ┴ ┴ ┴└──┘ └─────────────┘
st ──────────────────────────────────────┘└─────────────┘└─
197 haveI : compact_space (subtype s) := ⟨compact_iff_compact_univ.1 ‹compact s›⟩,
id └───────────┘ └─────┘ ┴ └──────────────────────┘ ┴└─────┘ ┴┴
src └──────┘└───────────┘┴ └─────┘┴ └───┘ └──────────────────────┘└─┘┴└─────┘┴ ┴┴
typ └──────┘└───────────┘┴ └─────┘┴┴└───┘ └──────────────────────┘└─┘┴└─────┘┴┴┴┴
doc └──────┘└───────────┘┴ ┴ └───┘ └─┘┴└─────┘┴ ┴┴
txt └──────┘ ┴ ┴ └───┘ └─┘ ┴ ┴
par └──────┘ ┴ ┴ └───┘ └─┘ ┴ ┴
pid ┴└┘ ┴ ┴ ┴└──┘ └─┘ ┴ ┴
st ──────────────────────────────────────────────────────────────────────────────┘└─
198 haveI : nonempty (subtype s) := ⟨Φ' xα⟩,
id └──────┘ └─────┘ ┴ └┘ └┘
src └──────┘└──────┘┴ └─────┘┴ └───┘ ┴ ┴
typ └──────┘└──────┘┴ └─────┘┴┴└───┘ └┘┴└┘┴
doc └──────┘ ┴ ┴ └───┘ ┴ ┴
txt └──────┘ ┴ ┴ └───┘ ┴ ┴
par └──────┘ ┴ ┴ └───┘ ┴ ┴
pid ┴└┘ ┴ ┴ ┴└──┘ ┴ ┴
st ────────────────────────────────────────┘└─
199 have ΦΦ' : Φ = subtype.val ∘ Φ', by { funext, refl },
id ┴ ┴ └─────────┘ ┴ └┘
src └─────────┘ ┴┴┴└─────────┘┴┴┴ └────┘ └───┘
typ └─────────┘┴┴┴┴└─────────┘┴┴┴└┘ └────┘ └───┘
doc └─────────┘ ┴ ┴ ┴ ┴ └────┘ └───┘
txt └─────────┘ ┴ ┴ ┴ ┴ └────┘ └───┘
par └─────────┘ ┴ ┴ ┴ ┴ └────┘ └───┘
pid └──────┘└─┘ ┴ ┴ ┴ ┴ ┴
st ────────────────────────────────┘ ┴└─────┘└─────┘└┘└
200 have ΨΨ' : Ψ = subtype.val ∘ Ψ', by { funext, refl },
id ┴ └─────────┘ └┘
src └─────────┘ ┴ ┴└─────────┘┴ ┴ └────┘ └───┘
typ └─────────┘┴┴ ┴└─────────┘┴ ┴└┘ └────┘ └───┘
doc └─────────┘ ┴ ┴ ┴ ┴ └────┘ └───┘
txt └─────────┘ ┴ ┴ ┴ ┴ └────┘ └───┘
par └─────────┘ ┴ ┴ ┴ ┴ └────┘ └───┘
pid └──────┘└─┘ ┴ ┴ ┴ ┴ ┴
st ────────────────────────────────┘ ┴└─────┘└─────┘└┘└
201 have : Hausdorff_dist (range Φ) (range Ψ) = Hausdorff_dist (range Φ') (range Ψ'),
id ┴ ┴ └────────────┘ └┘ └───┘ └┘
src └─────┘ ┴ ┴ └┘ ┴ └┘ ┴└────────────┘┴ ┴ └┘ └───┘┴ ┴
typ └─────┘ ┴ ┴┴└┘ ┴┴└┘ ┴└────────────┘┴ ┴└┘└┘ └───┘┴└┘┴
doc └─────┘ ┴ ┴ └┘ ┴ └┘ ┴└────────────┘┴ ┴ └┘ └───┘┴ ┴
txt └─────┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴
par └─────┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴
pid └───┘└┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴
st ─────────────────────────────────────────────────────────────────────────────────┘└─
202 { rw [ΦΦ', ΨΨ', range_comp, range_comp],
id └─┘ └─┘ └────────┘ └────────┘
src └──┘ └┘ └┘└────────┘└┘└────────┘┴
typ └──┘└─┘└┘└─┘└┘└────────┘└┘└────────┘┴
doc └──┘ └┘ └┘ └┘ ┴
txt └──┘ └┘ └┘ └┘ ┴
par └──┘ └┘ └┘ └┘ ┴
pid └┘ └┘ └┘ └┘ ┴
st ───┘└─────┘└───┘└──────────┘└──────────┘└──
203 exact Hausdorff_dist_image (isometry_subtype_val) },
id └──────────────────┘ └──────────────────┘
src └────┘└──────────────────┘┴ └──────────────────┘└┘
typ └────┘└──────────────────┘┴ └──────────────────┘└┘
doc └────┘└──────────────────┘┴ └──────────────────┘└┘
txt └────┘ ┴ └┘
par └────┘ ┴ └┘
pid ┴ ┴ ┴┴
st ─────────────────────────────────────────────────────┘└┘└
204 rw this,
id └──┘
src └─┘
typ └─┘└──┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ────────┘└─
205 -- Embed `s` in `ℓ^∞(ℝ)` through its Kuratowski embedding
st ────────────────────────────────────────────────────────────
206 let F := Kuratowski_embedding (subtype s),
id └──────────────────┘ └─────┘ ┴
src └───────┘└──────────────────┘┴ └─────┘┴ ┴
typ └───────┘└──────────────────┘┴ └─────┘┴┴┴
doc └───────┘└──────────────────┘┴ ┴ ┴
txt └───────┘ ┴ ┴ ┴
par └───────┘ ┴ ┴ ┴
pid └───┘┴└─┘ ┴ ┴ ┴
st ──────────────────────────────────────────┘└─
207 have : Hausdorff_dist (F '' (range Φ')) (F '' (range Ψ')) = Hausdorff_dist (range Φ') (range Ψ') :=
id └┘ ┴ └────────────┘ └┘ └───┘ └┘
src └─────┘ ┴ ┴└┘┴ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴└────────────┘┴ ┴ └┘ └───┘┴ └────
typ └─────┘ ┴ ┴└┘┴ ┴ └─┘ ┴┴ ┴ ┴ └─┘ ┴└────────────┘┴ ┴└┘└┘ └───┘┴└┘└────
doc └─────┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴└────────────┘┴ ┴ └┘ └───┘┴ └────
txt └─────┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ └────
par └─────┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ └────
pid └───┘└┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴└───
st ──────────────────────────────────────────────────────────────────────────────────────────────────────
208 Hausdorff_dist_image (Kuratowski_embedding.isometry _),
id └──────────────────┘ └───────────────────────────┘
src ───┘└──────────────────┘┴ └───────────────────────────┘└─┘
typ ───┘└──────────────────┘┴ └───────────────────────────┘└─┘
doc ───┘└──────────────────┘┴ └───────────────────────────┘└─┘
txt ───┘ ┴ └─┘
par ───┘ ┴ └─┘
pid ───┘ ┴ └─┘
st ─────────────────────────────────────────────────────────┘└─
209 rw ← this,
id └──┘
src └───┘
typ └───┘└──┘
doc └───┘
txt └───┘
par └───┘
pid └─┘
st ──────────┘└─
210 -- Let `A` and `B` be the images of `α` and `β` under this embedding. They are in `ℓ^∞(ℝ)`, and
st ──────────────────────────────────────────────────────────────────────────────────────────────────
211 -- their Hausdorff distance is the same as in the original space.
st ────────────────────────────────────────────────────────────────────
212 let A : nonempty_compacts ℓ_infty_ℝ := ⟨F '' (range Φ'), ⟨(range_nonempty _).image _,
id └───────────────┘ └───────┘ ┴ └───┘ └┘ └────────────┘
src └──────┘└───────────────┘┴└───────┘└──┘ ┴ ┴ └───┘┴ └─┘ └────────────┘└────────────
typ └──────┘└───────────────┘┴└───────┘└──┘ ┴┴ ┴ └───┘┴└┘└─┘ └────────────┘└────────────
doc └──────┘└───────────────┘┴└───────┘└──┘ ┴ ┴ └───┘┴ └─┘ └────────────
txt └──────┘ ┴ └──┘ ┴ ┴ ┴ └─┘ └────────────
par └──────┘ ┴ └──┘ ┴ ┴ ┴ └─┘ └────────────
pid └───┘└─┘ ┴ └──┘ ┴ ┴ ┴ └─┘ └────────────
st ────────────────────────────────────────────────────────────────────────────────────────
213 (compact_range IΦ'.continuous).image (Kuratowski_embedding.isometry _).continuous⟩⟩,
id └───────────┘ └────────────┘ └───────────────────────────┘
src ─────┘ └───────────┘┴└────────────┘└──────┘ └───────────────────────────┘└──────────────┘
typ ─────┘ └───────────┘┴└────────────┘└──────┘ └───────────────────────────┘└──────────────┘
doc ─────┘ ┴└────────────┘└──────┘ └───────────────────────────┘└──────────────┘
txt ─────┘ ┴ └──────┘ └──────────────┘
par ─────┘ ┴ └──────┘ └──────────────┘
pid ─────┘ ┴ └──────┘ └──────────────┘
st ────────────────────────────────────────────────────────────────────────────────────────┘└─
214 let B : nonempty_compacts ℓ_infty_ℝ := ⟨F '' (range Ψ'), ⟨(range_nonempty _).image _,
id └───────────────┘ └───────┘ ┴ └───┘ └┘ └────────────┘
src └──────┘└───────────────┘┴└───────┘└──┘ ┴ ┴ └───┘┴ └─┘ └────────────┘└────────────
typ └──────┘└───────────────┘┴└───────┘└──┘ ┴┴ ┴ └───┘┴└┘└─┘ └────────────┘└────────────
doc └──────┘└───────────────┘┴└───────┘└──┘ ┴ ┴ └───┘┴ └─┘ └────────────
txt └──────┘ ┴ └──┘ ┴ ┴ ┴ └─┘ └────────────
par └──────┘ ┴ └──┘ ┴ ┴ ┴ └─┘ └────────────
pid └───┘└─┘ ┴ └──┘ ┴ ┴ ┴ └─┘ └────────────
st ────────────────────────────────────────────────────────────────────────────────────────
215 (compact_range IΨ'.continuous).image (Kuratowski_embedding.isometry _).continuous⟩⟩,
id └───────────┘ └────────────┘ └───────────────────────────┘
src ─────┘ └───────────┘┴└────────────┘└──────┘ └───────────────────────────┘└──────────────┘
typ ─────┘ └───────────┘┴└────────────┘└──────┘ └───────────────────────────┘└──────────────┘
doc ─────┘ ┴└────────────┘└──────┘ └───────────────────────────┘└──────────────┘
txt ─────┘ ┴ └──────┘ └──────────────┘
par ─────┘ ┴ └──────┘ └──────────────┘
pid ─────┘ ┴ └──────┘ └──────────────┘
st ────────────────────────────────────────────────────────────────────────────────────────┘└─
216 have Aα : ⟦A⟧ = to_GH_space α,
id ┴┴┴ └─────────┘ ┴
src └────────┘┴ ┴┴ ┴└─────────┘┴
typ └────────┘┴┴┴┴ ┴└─────────┘┴┴
doc └────────┘ ┴ ┴└─────────┘┴
txt └────────┘ ┴ ┴ ┴
par └────────┘ ┴ ┴ ┴
pid └─────┘└─┘ ┴ ┴ ┴
st ──────────────────────────────┘└─
217 { rw eq_to_GH_space_iff,
id └────────────────┘
src └─┘└────────────────┘
typ └─┘└────────────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ───┘└───────────────────┘└─
218 exact ⟨λx, F (Φ' x), ⟨(Kuratowski_embedding.isometry _).comp IΦ', by rw range_comp⟩⟩ },
id ┴ └┘ └───────────────────────────┘ └─┘ └────────┘
src └────┘ └─┘ ┴ ┴ └─┘ └───────────────────────────┘└───────┘ └┘ ┴└─┘└────────┘└─┘
typ └────┘ └─┘┴┴ └┘┴ └─┘ └───────────────────────────┘└───────┘└─┘└┘ ┴└─┘└────────┘└─┘
doc └────┘ └─┘ ┴ ┴ └─┘ └───────────────────────────┘└───────┘ └┘ ┴└─┘ └─┘
txt └────┘ └─┘ ┴ ┴ └─┘ └───────┘ └┘ ┴└─┘ └─┘
par └────┘ └─┘ ┴ ┴ └─┘ └───────┘ └┘ ┴└─┘ └─┘
pid ┴ └─┘ ┴ ┴ └─┘ └───────┘ └┘ └──┘ └┘┴
st ───────────────────────────────────────────────────────────────────────┘└────────────┘└─┘└┘└
219 have Bβ : ⟦B⟧ = to_GH_space β,
id ┴ └─────────┘ ┴
src └────────┘ ┴ ┴└─────────┘┴
typ └────────┘ ┴ ┴ ┴└─────────┘┴┴
doc └────────┘ ┴ ┴└─────────┘┴
txt └────────┘ ┴ ┴ ┴
par └────────┘ ┴ ┴ ┴
pid └─────┘└─┘ ┴ ┴ ┴
st ──────────────────────────────┘└─
220 { rw eq_to_GH_space_iff,
id └────────────────┘
src └─┘└────────────────┘
typ └─┘└────────────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ───┘└───────────────────┘└─
221 exact ⟨λx, F (Ψ' x), ⟨(Kuratowski_embedding.isometry _).comp IΨ', by rw range_comp⟩⟩ },
id ┴ └┘ └───────────────────────────┘ └─┘ └────────┘
src └────┘ └─┘ ┴ ┴ └─┘ └───────────────────────────┘└───────┘ └┘ ┴└─┘└────────┘└─┘
typ └────┘ └─┘┴┴ └┘┴ └─┘ └───────────────────────────┘└───────┘└─┘└┘ ┴└─┘└────────┘└─┘
doc └────┘ └─┘ ┴ ┴ └─┘ └───────────────────────────┘└───────┘ └┘ ┴└─┘ └─┘
txt └────┘ └─┘ ┴ ┴ └─┘ └───────┘ └┘ ┴└─┘ └─┘
par └────┘ └─┘ ┴ ┴ └─┘ └───────┘ └┘ ┴└─┘ └─┘
pid ┴ └─┘ ┴ ┴ └─┘ └───────┘ └┘ └──┘ └┘┴
st ───────────────────────────────────────────────────────────────────────┘└────────────┘└─┘└┘└
222 refine cInf_le ⟨0,
id └─────┘
src └─────┘└─────┘┴ └──
typ └─────┘└─────┘┴ └──
doc └─────┘ ┴ └──
txt └─────┘ ┴ └──
par └─────┘ ┴ └──
pid ┴ ┴ └──
st ─────────────────────
223 begin simp [lower_bounds], assume t _ _ _ _ ht, rw ← ht, exact Hausdorff_dist_nonneg end⟩ _,
id └──────────┘ └┘ └───────────────────┘
src ───┘ ┴└────┘└──────────┘┴└┘└─────────────────┘└┘└───┘ └┘└────┘└───────────────────┘┴└────┘
typ ───┘ ┴└────┘└──────────┘┴└┘└─────────────────┘└┘└───┘└┘└──────┘└───────────────────┘└─────┘
doc ───┘ ┴└────┘└──────────┘┴└┘└─────────────────┘└┘└───┘ └┘└────┘└───────────────────┘┴└────┘
txt ───┘ ┴└────┘ ┴└┘└─────────────────┘└┘└───┘ └┘└────┘ ┴└────┘
par ───┘ ┴└────┘ ┴└┘└─────────────────┘└┘└───┘ └──────┘ └─────┘
pid ───┘ └─────┘ └───────────────────────────┘ └──────┘ └─────┘
st ───┘└───────────────────────┘└───────────────────┘└───────┘└────────────────────────────┘└─┘└─┘└─
224 apply (mem_image _ _ _).2,
id └───────┘
src └────┘ └───────┘└───────┘
typ └────┘ └───────┘└───────┘
doc └────┘ └───────┘
txt └────┘ └───────┘
par └────┘ └───────┘
pid ┴ └─────┘└┘
st ──────────────────────────┘└─
225 existsi (⟨A, B⟩ : nonempty_compacts ℓ_infty_ℝ × nonempty_compacts ℓ_infty_ℝ),
id ┴ ┴ ┴ └───────────────┘ └───────┘
src └──────┘ └┘ └──┘ ┴ ┴┴┴└───────────────┘┴└───────┘┴
typ └──────┘ ┴└┘┴└──┘ ┴ ┴┴┴└───────────────┘┴└───────┘┴
doc └──────┘ └┘ └──┘ ┴ ┴ ┴└───────────────┘┴└───────┘┴
txt └──────┘ └┘ └──┘ ┴ ┴ ┴ ┴ ┴
par └──────┘ └┘ └──┘ ┴ ┴ ┴ ┴ ┴
pid ┴ └┘ └──┘ ┴ ┴ ┴ ┴ ┴
st ─────────────────────────────────────────────────────────────────────────────┘└─
226 simp [Aα, Bβ]
id └┘ └┘
src └────┘ └┘ └┘
typ └────┘└┘└┘└┘└┘
doc └────┘ └┘ └┘
txt └────┘ └┘ └┘
par └────┘ └┘ └┘
pid ┴┴ └┘ ┴┴
st ───────────────┘
227 end
st └─┘
228
229 local attribute [instance, priority 10] inhabited_of_nonempty'
id └────────────────────┘
src └────────────────────┘
typ └────────────────────┘
230
231 /-- The optimal coupling constructed above realizes exactly the Gromov-Hausdorff distance,
232 essentially by design. -/
233 lemma Hausdorff_dist_optimal {α : Type u} [metric_space α] [compact_space α] [nonempty α]
id └──────────┘ ┴ └───────────┘ ┴ └──────┘ ┴
src └──────────┘ └───────────┘ └──────┘
typ └──────────┘ ┴ └───────────┘ ┴ └──────┘ ┴
doc └──────────┘ └───────────┘
234 {β : Type v} [metric_space β] [compact_space β] [nonempty β] :
id └──────────┘ ┴ └───────────┘ ┴ └──────┘ ┴
src └──────────┘ └───────────┘ └──────┘
typ └──────────┘ ┴ └───────────┘ ┴ └──────┘ ┴
doc └──────────┘ └───────────┘
235 Hausdorff_dist (range (optimal_GH_injl α β)) (range (optimal_GH_injr α β)) = GH_dist α β :=
id └────────────┘ └───┘ └─────────────┘ ┴ ┴ └───┘ └─────────────┘ ┴ ┴ ┴ └─────┘ ┴ ┴
src └────────────┘ └───┘ └─────────────┘ └───┘ └─────────────┘ ┴ └─────┘
typ └────────────┘ └───┘ └─────────────┘ ┴ ┴ └───┘ └─────────────┘ ┴ ┴ ┴ └─────┘ ┴ ┴
doc └────────────┘ └───┘ └─────────────┘ └───┘ └─────────────┘ └─────┘
236 begin
st └─────
237 /- we only need to check the inequality `≤`, as the other one follows from the previous lemma.
st ─────────────────────────────────────────────────────────────────────────────────────────────────
238 As the Gromov-Hausdorff distance is an infimum, we need to check that the Hausdorff distance
st ──────────────────────────────────────────────────────────────────────────────────────────────────
239 in the optimal coupling is smaller than the Hausdorff distance of any coupling.
st ─────────────────────────────────────────────────────────────────────────────────────
240 First, we check this for couplings which already have small Hausdorff distance: in this
st ─────────────────────────────────────────────────────────────────────────────────────────────
241 case, the induced "distance" on `α ⊕ β` belongs to the candidates family introduced in the
st ────────────────────────────────────────────────────────────────────────────────────────────────
242 definition of the optimal coupling, and the conclusion follows from the optimality
st ────────────────────────────────────────────────────────────────────────────────────────
243 of the optimal coupling within this family.
st ─────────────────────────────────────────────────
244 -/
st ─────
245 have A : ∀p q : nonempty_compacts (ℓ_infty_ℝ), ⟦p⟧ = to_GH_space α → ⟦q⟧ = to_GH_space β →
id └───────────────┘ └───────┘ ┴ ┴ ┴ ┴ └─────────┘
src └───────┘ └────┘└───────────────┘┴ └───────┘┴ ┴┴ ┴┴┴┴ ┴ ┴ ┴ ┴ ┴└─────────┘┴ ┴ └
typ └───────┘ └────┘└───────────────┘┴ └───────┘┴ ┴┴ ┴┴┴┴ ┴ ┴ ┴ ┴┴┴└─────────┘┴ ┴ └
doc └───────┘ └────┘└───────────────┘┴ └───────┘┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴└─────────┘┴ ┴ └
txt └───────┘ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └
par └───────┘ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └
pid └────┘└─┘ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └
st ─────────────────────────────────────────────────────────────────────────────────────────────
246 Hausdorff_dist (p.val) (q.val) < diam (univ : set α) + 1 + diam (univ : set β) →
id └──┘ └──┘ ┴ ┴ └──┘ └──┘ └─┘
src ───────┘ ┴ └──┘└┘ └──┘└┘┴┴ ┴ └─┘ ┴ └┘┴└─┘ ┴└──┘┴ └──┘└─┘└─┘┴ └┘ └
typ ───────┘ ┴ └──┘└┘ └──┘└┘┴┴ ┴ └─┘ ┴ └┘┴└─┘ ┴└──┘┴ └──┘└─┘└─┘┴ └┘ └
doc ───────┘ ┴ └┘ └┘ ┴ ┴ └─┘ ┴ └┘ └─┘ ┴└──┘┴ └─┘ ┴ └┘ └
txt ───────┘ ┴ └┘ └┘ ┴ ┴ └─┘ ┴ └┘ └─┘ ┴ ┴ └─┘ ┴ └┘ └
par ───────┘ ┴ └┘ └┘ ┴ ┴ └─┘ ┴ └┘ └─┘ ┴ ┴ └─┘ ┴ └┘ └
pid ───────┘ ┴ └┘ └┘ ┴ ┴ └─┘ ┴ └┘ └─┘ ┴ ┴ └─┘ ┴ └┘ └
st ─────────────────────────────────────────────────────────────────────────────────────────
247 Hausdorff_dist (range (optimal_GH_injl α β)) (range (optimal_GH_injr α β)) ≤ Hausdorff_dist (p.val) (q.val),
id └─────────────┘ └───┘ └─────────────┘ ┴ ┴ ┴ └────────────┘ └──┘
src ───────┘ ┴ ┴ └─────────────┘┴ ┴ └─┘ └───┘┴ └─────────────┘┴ ┴ └─┘┴┴└────────────┘┴ └──┘└┘ ┴
typ ───────┘ ┴ ┴ └─────────────┘┴ ┴ └─┘ └───┘┴ └─────────────┘┴┴┴┴└─┘┴┴└────────────┘┴ └──┘└┘ ┴
doc ───────┘ ┴ ┴ └─────────────┘┴ ┴ └─┘ └───┘┴ └─────────────┘┴ ┴ └─┘ ┴└────────────┘┴ └┘ ┴
txt ───────┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ └┘ ┴
par ───────┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ └┘ ┴
pid ───────┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ └┘ ┴
st ──────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘└─
248 { assume p q hp hq bound,
src └────────────────────┘
typ └────────────────────┘
doc └────────────────────┘
txt └────────────────────┘
par └────────────────────┘
pid └────────────────────┘
st ───┘└────────────────────┘└─
249 rcases eq_to_GH_space_iff.1 hp with ⟨Φ, ⟨Φisom, Φrange⟩⟩,
id └────────────────┘ └┘
src └─────┘└────────────────┘└─┘ └────────────────────────┘
typ └─────┘└────────────────┘└─┘└┘└────────────────────────┘
doc └─────┘ └─┘ └────────────────────────┘
txt └─────┘ └─┘ └────────────────────────┘
par └─────┘ └─┘ └────────────────────────┘
pid ┴ └─┘ └────────────────────────┘
st ───────────────────────────────────────────────────────────┘└─
250 rcases eq_to_GH_space_iff.1 hq with ⟨Ψ, ⟨Ψisom, Ψrange⟩⟩,
id └────────────────┘ └┘
src └─────┘└────────────────┘└─┘ └────────────────────────┘
typ └─────┘└────────────────┘└─┘└┘└────────────────────────┘
doc └─────┘ └─┘ └────────────────────────┘
txt └─────┘ └─┘ └────────────────────────┘
par └─────┘ └─┘ └────────────────────────┘
pid ┴ └─┘ └────────────────────────┘
st ───────────────────────────────────────────────────────────┘└─
251 have I : diam (range Φ ∪ range Ψ) ≤ 2 * diam (univ : set α) + 1 + 2 * diam (univ : set β),
id ┴ ┴ └───┘ ┴ ┴ ┴ └──┘ └──┘ └─┘ ┴
src └───────┘ ┴ ┴ ┴┴┴└───┘┴ └┘ └─┘┴┴ ┴ └─┘ ┴ └┘ └─┘ └─┘ ┴└──┘┴ └──┘└─┘└─┘┴ ┴
typ └───────┘ ┴ ┴┴┴┴┴└───┘┴┴└┘ └─┘┴┴ ┴ └─┘ ┴┴└┘ └─┘ └─┘ ┴└──┘┴ └──┘└─┘└─┘┴┴┴
doc └───────┘ ┴ ┴ ┴ ┴└───┘┴ └┘ └─┘ ┴ ┴ └─┘ ┴ └┘ └─┘ └─┘ ┴└──┘┴ └─┘ ┴ ┴
txt └───────┘ ┴ ┴ ┴ ┴ ┴ └┘ └─┘ ┴ ┴ └─┘ ┴ └┘ └─┘ └─┘ ┴ ┴ └─┘ ┴ ┴
par └───────┘ ┴ ┴ ┴ ┴ ┴ └┘ └─┘ ┴ ┴ └─┘ ┴ └┘ └─┘ └─┘ ┴ ┴ └─┘ ┴ ┴
pid └────┘└─┘ ┴ ┴ ┴ ┴ ┴ └┘ └─┘ ┴ ┴ └─┘ ┴ └┘ └─┘ └─┘ ┴ ┴ └─┘ ┴ ┴
st ────────────────────────────────────────────────────────────────────────────────────────────┘└─
252 { rcases exists_mem_of_nonempty α with ⟨xα, _⟩,
id └────────────────────┘ ┴
src └─────┘└────────────────────┘┴ └───────────┘
typ └─────┘└────────────────────┘┴┴└───────────┘
doc └─────┘ ┴ └───────────┘
txt └─────┘ ┴ └───────────┘
par └─────┘ ┴ └───────────┘
pid ┴ ┴ └───────────┘
st ─────┘└──────────────────────────────────────────┘└─
253 have : ∃y ∈ range Ψ, dist (Φ xα) y < diam (univ : set α) + 1 + diam (univ : set β),
id ┴ └───┘ ┴┴ └──┘ ┴ └┘ ┴ └──┘ └──┘ └─┘ ┴
src └─────┘┴└──┘└───┘┴ ┴┴└──┘┴ ┴ └┘ ┴ ┴ ┴ └─┘ ┴ └┘ └─┘ ┴└──┘┴ └──┘└─┘└─┘┴ ┴
typ └─────┘┴└──┘└───┘┴┴┴┴└──┘┴ ┴┴└┘└┘ ┴ ┴ ┴ └─┘ ┴┴└┘ └─┘ ┴└──┘┴ └──┘└─┘└─┘┴┴┴
doc └─────┘ └──┘└───┘┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └─┘ ┴ └┘ └─┘ ┴└──┘┴ └─┘ ┴ ┴
txt └─────┘ └──┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └─┘ ┴ └┘ └─┘ ┴ ┴ └─┘ ┴ ┴
par └─────┘ └──┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └─┘ ┴ └┘ └─┘ ┴ ┴ └─┘ ┴ ┴
pid └───┘└┘ └──┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └─┘ ┴ └┘ └─┘ ┴ ┴ └─┘ ┴ ┴
st ───────────────────────────────────────────────────────────────────────────────────────┘└─
254 { rw Ψrange,
id └────┘
src └─┘
typ └─┘└────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ───────┘└───────┘└─
255 have : Φ xα ∈ p.val := begin rw ← Φrange, exact mem_range_self _ end,
id ┴ └┘ └───┘ └────┘ └────────────┘
src └─────┘ ┴ ┴ ┴└───┘└──┘ ┴└───┘ └┘└────┘└────────────┘└─┘└─┘
typ └─────┘┴┴└┘┴ ┴└───┘└──┘ ┴└───┘└────┘└┘└────┘└────────────┘└─┘└─┘
doc └─────┘ ┴ ┴ ┴ └──┘ ┴└───┘ └┘└────┘ └─┘└─┘
txt └─────┘ ┴ ┴ ┴ └──┘ ┴└───┘ └┘└────┘ └─┘└─┘
par └─────┘ ┴ ┴ ┴ └──┘ ┴└───┘ └┘└────┘ └─┘└─┘
pid └───┘└┘ ┴ ┴ ┴ └──┘ └────┘ └──────┘ └────┘
st ──────────────────────────────┘└───────────────┘└───────────────────────┘└─┘└─
256 exact exists_dist_lt_of_Hausdorff_dist_lt this bound
id └─────────────────────────────────┘ └──┘ └───┘
src └────┘└─────────────────────────────────┘┴ ┴ └
typ └────┘└─────────────────────────────────┘┴└──┘┴└───┘└
doc └────┘└─────────────────────────────────┘┴ ┴ └
txt └────┘ ┴ ┴ └
par └────┘ ┴ ┴ └
pid ┴ ┴ ┴ └
st ─────────────────────────────────────────────────────────────
257 (Hausdorff_edist_ne_top_of_nonempty_of_bounded p.2.1 q.2.1 p.2.2.bounded q.2.2.bounded) },
id └───────────────────────────────────────────┘ ┴ ┴
src ─────────┘ └───────────────────────────────────────────┘┴ └───┘ └───┘ └───────────┘ └────────────┘
typ ─────────┘ └───────────────────────────────────────────┘┴ └───┘ └───┘┴└───────────┘┴└────────────┘
doc ─────────┘ └───────────────────────────────────────────┘┴ └───┘ └───┘ └───────────┘ └────────────┘
txt ─────────┘ ┴ └───┘ └───┘ └───────────┘ └────────────┘
par ─────────┘ ┴ └───┘ └───┘ └───────────┘ └────────────┘
pid ─────────┘ ┴ └───┘ └───┘ └───────────┘ └───────────┘┴
st ─────────────────────────────────────────────────────────────────────────────────────────────────┘└┘└
258 rcases this with ⟨y, hy, dy⟩,
id └──┘
src └─────┘ └───────────────┘
typ └─────┘└──┘└───────────────┘
doc └─────┘ └───────────────┘
txt └─────┘ └───────────────┘
par └─────┘ └───────────────┘
pid ┴ └───────────────┘
st ─────────────────────────────────┘└─
259 rcases mem_range.1 hy with ⟨z, hzy⟩,
id └───────┘ └┘
src └─────┘└───────┘└─┘ └────────────┘
typ └─────┘└───────┘└─┘└┘└────────────┘
doc └─────┘ └─┘ └────────────┘
txt └─────┘ └─┘ └────────────┘
par └─────┘ └─┘ └────────────┘
pid ┴ └─┘ └────────────┘
st ────────────────────────────────────────┘└─
260 rw ← hzy at dy,
id └─┘
src └───┘ └────┘
typ └───┘└─┘└────┘
doc └───┘ └────┘
txt └───┘ └────┘
par └───┘ └────┘
pid └─┘ └────┘
st ───────────────────┘└─
261 have DΦ : diam (range Φ) = diam (univ : set α) :=
id └───┘ ┴ └──┘ └──┘ └─┘ ┴
src └────────┘ ┴ └───┘┴ └┘ ┴└──┘┴ └──┘└─┘└─┘┴ └────
typ └────────┘ ┴ └───┘┴┴└┘ ┴└──┘┴ └──┘└─┘└─┘┴┴└────
doc └────────┘ ┴ └───┘┴ └┘ ┴└──┘┴ └─┘ ┴ └────
txt └────────┘ ┴ ┴ └┘ ┴ ┴ └─┘ ┴ └────
par └────────┘ ┴ ┴ └┘ ┴ ┴ └─┘ ┴ └────
pid └─────┘└─┘ ┴ ┴ └┘ ┴ ┴ └─┘ ┴ ┴└───
st ────────────────────────────────────────────────────────
262 begin rw [← image_univ], apply metric.isometry.diam_image Φisom end,
id └────────┘ └────────────────────────┘ └───┘
src ───────┘ ┴└────┘└────────┘┴└┘└────┘└────────────────────────┘┴ ┴└─┘
typ ───────┘ ┴└────┘└────────┘┴└┘└────┘└────────────────────────┘┴└───┘┴└─┘
doc ───────┘ ┴└────┘ ┴└┘└────┘└────────────────────────┘┴ ┴└─┘
txt ───────┘ ┴└────┘ ┴└┘└────┘ ┴ ┴└─┘
par ───────┘ ┴└────┘ ┴└┘└────┘ ┴ ┴└─┘
pid ───────┘ └─────┘ └───────┘ ┴ └──┘
st ───────┘└────────────────────┘└────────────────────────────────────────┘└─┘└─
263 have DΨ : diam (range Ψ) = diam (univ : set β) :=
id └───┘ ┴ └──┘ └──┘ └─┘ ┴
src └────────┘ ┴ └───┘┴ └┘ ┴└──┘┴ └──┘└─┘└─┘┴ └────
typ └────────┘ ┴ └───┘┴┴└┘ ┴└──┘┴ └──┘└─┘└─┘┴┴└────
doc └────────┘ ┴ └───┘┴ └┘ ┴└──┘┴ └─┘ ┴ └────
txt └────────┘ ┴ ┴ └┘ ┴ ┴ └─┘ ┴ └────
par └────────┘ ┴ ┴ └┘ ┴ ┴ └─┘ ┴ └────
pid └─────┘└─┘ ┴ ┴ └┘ ┴ ┴ └─┘ ┴ ┴└───
st ────────────────────────────────────────────────────────
264 begin rw [← image_univ], apply metric.isometry.diam_image Ψisom end,
id └────────┘ └────────────────────────┘ └───┘
src ───────┘ ┴└────┘└────────┘┴└┘└────┘└────────────────────────┘┴ ┴└─┘
typ ───────┘ ┴└────┘└────────┘┴└┘└────┘└────────────────────────┘┴└───┘┴└─┘
doc ───────┘ ┴└────┘ ┴└┘└────┘└────────────────────────┘┴ ┴└─┘
txt ───────┘ ┴└────┘ ┴└┘└────┘ ┴ ┴└─┘
par ───────┘ ┴└────┘ ┴└┘└────┘ ┴ ┴└─┘
pid ───────┘ └─────┘ └───────┘ ┴ └──┘
st ───────┘└────────────────────┘└────────────────────────────────────────┘└─┘└─
265 calc
id └──┘
src └──┘
typ └──┘
doc └──┘
st ───────────
266 diam (range Φ ∪ range Ψ) ≤ diam (range Φ) + dist (Φ xα) (Ψ z) + diam (range Ψ) :
id └──┘ ┴ └┘ ┴ └──┘ └───┘ ┴
src └──┘ └──┘ └───┘
typ └──┘ ┴ └┘ ┴ └──┘ └───┘ ┴
doc └──┘ └───┘
st ─────────────────────────────────────────────────────────────────────────────────────────
267 diam_union (mem_range_self _) (mem_range_self _)
id └────────┘ └────────────┘
src └────────┘ └────────────┘
typ └────────┘ └────────────┘
doc └────────┘
st ───────────────────────────────────────────────────────────
268 ... ≤ diam (univ : set α) + (diam (univ : set α) + 1 + diam (univ : set β)) + diam (univ : set β) :
st ────────────────────────────────────────────────────────────────────────────────────────────────────────────
269 by { rw [DΦ, DΨ], apply add_le_add (add_le_add (le_refl _) (le_of_lt dy)) (le_refl _) }
id └┘ └┘ └────────┘ └──────┘ └┘ └─────┘
src └──┘ └┘ ┴ └────┘ ┴ └────────┘┴ └──┘ └──────┘┴ └─┘ └─────┘└──┘
typ └──┘└┘└┘└┘┴ └────┘ ┴ └────────┘┴ └──┘ └──────┘┴└┘└─┘ └─────┘└──┘
doc └──┘ └┘ ┴ └────┘ ┴ ┴ └──┘ ┴ └─┘ └──┘
txt └──┘ └┘ ┴ └────┘ ┴ ┴ └──┘ ┴ └─┘ └──┘
par └──┘ └┘ ┴ └────┘ ┴ ┴ └──┘ ┴ └─┘ └──┘
pid └┘ └┘ ┴ ┴ ┴ ┴ └──┘ ┴ └─┘ └─┘┴
st ───────────┘└───────┘└──┘└─────────────────────────────────────────────────────────────────────┘└┘
270 ... = 2 * diam (univ : set α) + 1 + 2 * diam (univ : set β) : by ring },
id ┴ └──┘ └─┘ ┴
src └──┘ └─┘ └───┘
typ ┴ └──┘ └─┘ ┴ └───┘
doc └───┘
txt └───┘
par └───┘
pid ┴
st └──────────────────────────────────────────────────────────────────────┘└────┘└┘└
271
st ─
272 let f : α ⊕ β → ℓ_infty_ℝ := λx, match x with | inl y := Φ y | inr z := Ψ z end,
id ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴
src └──────┘ ┴┴┴ ┴ ┴└───────┘└──┘ └─┘ ┴ └──────┘ ┴ └──┘ ┴ └─┘ ┴ └──┘ ┴ └──┘
typ └──────┘┴┴┴┴┴┴ ┴└───────┘└──┘ └─┘ ┴ └──────┘ ┴┴└──┘┴┴ └─┘ ┴┴└──┘┴┴ └──┘
doc └──────┘ ┴ ┴ ┴ ┴└───────┘└──┘ └─┘ ┴ └──────┘ ┴ └──┘ ┴ └─┘ ┴ └──┘ ┴ └──┘
txt └──────┘ ┴ ┴ ┴ ┴ └──┘ └─┘ ┴ └──────┘ ┴ └──┘ ┴ └─┘ ┴ └──┘ ┴ └──┘
par └──────┘ ┴ ┴ ┴ ┴ └──┘ └─┘ ┴ └──────┘ ┴ └──┘ ┴ └─┘ ┴ └──┘ ┴ └──┘
pid └───┘└─┘ ┴ ┴ ┴ ┴ └──┘ └─┘ ┴ └──────┘ ┴ └──┘ ┴ └─┘ ┴ └──┘ ┴ └──┘
st ──────────────────────────────────────────────────────────────────────────────────┘└─
273 let F : (α ⊕ β) × (α ⊕ β) → ℝ := λp, dist (f p.1) (f p.2),
id ┴ ┴ ┴ └──┘ ┴
src └──────┘ ┴ ┴ └┘┴┴ ┴ ┴ └┘ ┴ └──┘ └─┘└──┘┴ ┴ └──┘ ┴ └─┘
typ └──────┘ ┴ ┴ └┘┴┴ ┴┴ ┴┴└┘ ┴ └──┘ └─┘└──┘┴ ┴ └──┘ ┴┴ └─┘
doc └──────┘ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ └──┘ └─┘ ┴ ┴ └──┘ ┴ └─┘
txt └──────┘ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ └──┘ └─┘ ┴ ┴ └──┘ ┴ └─┘
par └──────┘ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ └──┘ └─┘ ┴ ┴ └──┘ ┴ └─┘
pid └───┘└─┘ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ └──┘ └─┘ ┴ ┴ └──┘ ┴ └─┘
st ────────────────────────────────────────────────────────────┘└─
274 -- check that the induced "distance" is a candidate
st ────────────────────────────────────────────────────────
275 have Fgood : F ∈ candidates α β,
id ┴ └────────┘ ┴ ┴
src └───────────┘ ┴ ┴└────────┘┴ ┴
typ └───────────┘┴┴ ┴└────────┘┴┴┴┴
doc └───────────┘ ┴ ┴└────────┘┴ ┴
txt └───────────┘ ┴ ┴ ┴ ┴
par └───────────┘ ┴ ┴ ┴ ┴
pid └────────┘└─┘ ┴ ┴ ┴ ┴
st ──────────────────────────────────┘└─
276 { simp only [candidates, forall_const, and_true, add_comm, eq_self_iff_true, dist_eq_zero,
id └────────┘ └──────────┘ └──────┘ └──────┘ └──────────────┘ └──────────┘
src └─────────┘└────────┘└┘└──────────┘└┘└──────┘└┘└──────┘└┘└──────────────┘└┘└──────────┘└─
typ └─────────┘└────────┘└┘└──────────┘└┘└──────┘└┘└──────┘└┘└──────────────┘└┘└──────────┘└─
doc └─────────┘└────────┘└┘ └┘ └┘ └┘ └┘ └─
txt └─────────┘ └┘ └┘ └┘ └┘ └┘ └─
par └─────────┘ └┘ └┘ └┘ └┘ └┘ └─
pid ┴└──┘└┘ └┘ └┘ └┘ └┘ └┘ └─
st ─────┘└────────────────────────────────────────────────────────────────────────────────────────
277 and_self, set.mem_set_of_eq],
id └──────┘ └───────────────┘
src ────────────────┘└──────┘└┘└───────────────┘┴
typ ────────────────┘└──────┘└┘└───────────────┘┴
doc ────────────────┘ └┘ ┴
txt ────────────────┘ └┘ ┴
par ────────────────┘ └┘ ┴
pid ────────────────┘ └┘ ┴
st ────────────────────────────────────────────┘└─
278 repeat {split},
src └──────┘└───┘┴
typ └──────┘└───┘┴
doc └──────┘└───┘┴
txt └──────┘└───┘┴
par └──────┘└───┘┴
pid └──────┘
st ──────────────────┘└┘└
279 { exact λx y, calc
src └────┘ └───┘ └
typ └────┘ └───┘ └
doc └────┘ └───┘ └
txt └────┘ └───┘ └
par └────┘ └───┘ └
pid ┴ └───┘ └
st ───────┘└────────────────
280 F (inl x, inl y) = dist (Φ x) (Φ y) : rfl
id ┴ └─┘ ┴ └─┘
src ───────┘ ┴ ┴ └┘└─┘┴ └┘ ┴ ┴ ┴ └┘ ┴ └──┘└─┘└
typ ───────┘┴┴ ┴ └┘└─┘┴ └┘ ┴ ┴ ┴ └┘ ┴┴ └──┘└─┘└
doc ───────┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └┘ ┴ └──┘ └
txt ───────┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └┘ ┴ └──┘ └
par ───────┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └┘ ┴ └──┘ └
pid ───────┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └┘ ┴ └──┘ └
st ──────────────────────────────────────────────────
281 ... = dist x y : Φisom.dist_eq },
id └──┘ └───────────┘
src ───────────┘ ┴└──┘┴ ┴ └─┘└───────────┘┴
typ ───────────┘ ┴└──┘┴ ┴ └─┘└───────────┘┴
doc ───────────┘ ┴ ┴ ┴ └─┘└───────────┘┴
txt ───────────┘ ┴ ┴ ┴ └─┘ ┴
par ───────────┘ ┴ ┴ ┴ └─┘ ┴
pid ───────────┘ ┴ ┴ ┴ └─┘ ┴
st ──────────────────────────────────────┘└┘└
282 { exact λx y, calc
src └────┘ └───┘ └
typ └────┘ └───┘ └
doc └────┘ └───┘ └
txt └────┘ └───┘ └
par └────┘ └───┘ └
pid ┴ └───┘ └
st ───────┘└────────────────
283 F (inr x, inr y) = dist (Ψ x) (Ψ y) : rfl
id ┴ └─┘ ┴ └─┘
src ───────┘ ┴ ┴ └┘└─┘┴ └┘ ┴ ┴ ┴ └┘ ┴ └──┘└─┘└
typ ───────┘┴┴ ┴ └┘└─┘┴ └┘ ┴ ┴ ┴ └┘ ┴┴ └──┘└─┘└
doc ───────┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └┘ ┴ └──┘ └
txt ───────┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └┘ ┴ └──┘ └
par ───────┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └┘ ┴ └──┘ └
pid ───────┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └┘ ┴ └──┘ └
st ──────────────────────────────────────────────────
284 ... = dist x y : Ψisom.dist_eq },
id └──┘ └───────────┘
src ───────────┘ ┴└──┘┴ ┴ └─┘└───────────┘┴
typ ───────────┘ ┴└──┘┴ ┴ └─┘└───────────┘┴
doc ───────────┘ ┴ ┴ ┴ └─┘└───────────┘┴
txt ───────────┘ ┴ ┴ ┴ └─┘ ┴
par ───────────┘ ┴ ┴ ┴ └─┘ ┴
pid ───────────┘ ┴ ┴ ┴ └─┘ ┴
st ──────────────────────────────────────┘└┘└
285 { exact λx y, dist_comm _ _ },
id └───────┘
src └────┘ └───┘└───────┘└───┘
typ └────┘ └───┘└───────┘└───┘
doc └────┘ └───┘ └───┘
txt └────┘ └───┘ └───┘
par └────┘ └───┘ └───┘
pid ┴ └───┘ └──┘┴
st ───────┘└────────────────────────┘└┘└
286 { exact λx y z, dist_triangle _ _ _ },
id └───────────┘
src └────┘ └─────┘└───────────┘└─────┘
typ └────┘ └─────┘└───────────┘└─────┘
doc └────┘ └─────┘ └─────┘
txt └────┘ └─────┘ └─────┘
par └────┘ └─────┘ └─────┘
pid ┴ └─────┘ └────┘┴
st ───────┘└────────────────────────────────┘└┘└
287 { exact λx y, calc
src └────┘ └───┘ └
typ └────┘ └───┘ └
doc └────┘ └───┘ └
txt └────┘ └───┘ └
par └────┘ └───┘ └
pid ┴ └───┘ └
st ─────────────────────────
288 F (x, y) ≤ diam (range Φ ∪ range Ψ) :
id ┴ ┴ └───┘ ┴
src ───────┘ ┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴└───┘┴ └───
typ ───────┘┴┴ └┘ └┘ ┴ ┴ ┴┴┴ ┴└───┘┴┴└───
doc ───────┘ ┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴└───┘┴ └───
txt ───────┘ ┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └───
par ───────┘ ┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └───
pid ───────┘ ┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └───
st ──────────────────────────────────────────────
289 begin
src ───────┘ └
typ ───────┘ └
doc ───────┘ └
txt ───────┘ └
par ───────┘ └
pid ───────┘ └
st ───────┘└─────
290 have A : ∀z : α ⊕ β, f z ∈ range Φ ∪ range Ψ,
id ┴ ┴ ┴ ┴ └───┘ ┴
src ─────────┘└───────┘ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴└───┘┴ └─
typ ─────────┘└───────┘ └──┘┴┴ ┴┴ ┴┴┴ ┴ ┴ ┴┴┴ ┴└───┘┴┴└─
doc ─────────┘└───────┘ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴└───┘┴ └─
txt ─────────┘└───────┘ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─
par ─────────┘└───────┘ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─
pid ──────────────────┘ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─
st ─────────────────────────────────────────────────────┘└─
291 { assume z,
src ───────────┘└──────┘└─
typ ───────────┘└──────┘└─
doc ───────────┘└──────┘└─
txt ───────────┘└──────┘└─
par ───────────┘└──────┘└─
pid ──────────────────────
st ──────────┘└───────┘└─
292 cases z,
id ┴
src ───────────┘└────┘ └─
typ ───────────┘└────┘┴└─
doc ───────────┘└────┘ └─
txt ───────────┘└────┘ └─
par ───────────┘└────┘ └─
pid ─────────────────┘ └─
st ──────────────────┘└─
293 { apply mem_union_left, apply mem_range_self },
id └────────────┘ └────────────┘
src ─────────────┘└────┘└────────────┘└┘└────┘└────────────┘┴└──
typ ───────────────────┘└────────────┘└──────┘└────────────┘└───
doc ─────────────┘└────┘ └┘└────┘ ┴└──
txt ─────────────┘└────┘ └┘└────┘ ┴└──
par ───────────────────┘ └──────┘ └───
pid ───────────────────┘ └──────┘ └───
st ────────────┘└───────────────────┘└─────────────────────┘┴└─
294 { apply mem_union_right, apply mem_range_self } },
id └─────────────┘ └────────────┘
src ─────────────┘└────┘└─────────────┘└┘└────┘└────────────┘┴└────
typ ───────────────────┘└─────────────┘└──────┘└────────────┘└─────
doc ─────────────┘└────┘ └┘└────┘ ┴└────
txt ─────────────┘└────┘ └┘└────┘ ┴└────
par ───────────────────┘ └──────┘ └─────
pid ───────────────────┘ └──────┘ └─────
st ──────────────────────────────────┘└─────────────────────┘└─┘└─
295 refine dist_le_diam_of_mem _ (A _) (A _),
id └─────────────────┘ ┴
src ─────────┘└─────┘└─────────────────┘└─┘ └──┘ └─┘└─
typ ────────────────┘└─────────────────┘└─┘ └──┘ ┴└────
doc ─────────┘└─────┘└─────────────────┘└─┘ └──┘ └─┘└─
txt ─────────┘└─────┘ └─┘ └──┘ └─┘└─
par ────────────────┘ └─┘ └──┘ └────
pid ────────────────┘ └─┘ └──┘ └────
st ─────────────────────────────────────────────────┘└─
296 rw [Φrange, Ψrange],
id └────┘ └────┘
src ─────────┘└──┘ └┘ ┴└─
typ ─────────┘└──┘└────┘└┘└────┘┴└─
doc ─────────┘└──┘ └┘ ┴└─
txt ─────────┘└──┘ └┘ ┴└─
par ─────────┘└──┘ └┘ ┴└─
pid ─────────────┘ └┘ └──
st ───────────────────┘└──────┘└──
297 exact (p.2.2.union q.2.2).bounded,
id ┴ ┴
src ───────────────┘ └─────────┘ └──────────────
typ ───────────────┘ ┴└─────────┘┴└──────────────
doc ───────────────┘ └─────────┘ └──────────────
txt ───────────────┘ └─────────┘ └──────────────
par ───────────────┘ └─────────┘ └──────────────
pid ───────────────┘ └─────────┘ └──────────────
st ──────────────────────────────────────────┘└─
298 end
src ────────────
typ ────────────
doc ────────────
txt ────────────
par ────────────
pid ────────────
st ──────────┘└
299 ... ≤ 2 * diam (univ : set α) + 1 + 2 * diam (univ : set β) : I } },
id ┴ └──┘ └──┘ └─┘ ┴ ┴
src ───────────┘ └─┘ ┴ ┴ └─┘ ┴ └┘ └─┘ └─┘ ┴└──┘┴ └──┘└─┘└─┘┴ └──┘ ┴
typ ───────────┘ └─┘ ┴ ┴ └─┘ ┴┴└┘ └─┘ └─┘ ┴└──┘┴ └──┘└─┘└─┘┴┴└──┘┴┴
doc ───────────┘ └─┘ ┴ ┴ └─┘ ┴ └┘ └─┘ └─┘ ┴└──┘┴ └─┘ ┴ └──┘ ┴
txt ───────────┘ └─┘ ┴ ┴ └─┘ ┴ └┘ └─┘ └─┘ ┴ ┴ └─┘ ┴ └──┘ ┴
par ───────────┘ └─┘ ┴ ┴ └─┘ ┴ └┘ └─┘ └─┘ ┴ ┴ └─┘ ┴ └──┘ ┴
pid ───────────┘ └─┘ ┴ ┴ └─┘ ┴ └┘ └─┘ └─┘ ┴ ┴ └─┘ ┴ └──┘ ┴
st ───────────────────────────────────────────────────────────────────────┘└──┘└
300 let Fb := candidates_b_of_candidates F Fgood,
id └────────────────────────┘ ┴ └───┘
src └────────┘└────────────────────────┘┴ ┴
typ └────────┘└────────────────────────┘┴┴┴└───┘
doc └────────┘└────────────────────────┘┴ ┴
txt └────────┘ ┴ ┴
par └────────┘ ┴ ┴
pid └────┘┴└─┘ ┴ ┴
st ───────────────────────────────────────────────┘└─
301 have : Hausdorff_dist (range (optimal_GH_injl α β)) (range (optimal_GH_injr α β)) ≤ HD Fb :=
id └────────────┘ └─────────────┘ └───┘ └─────────────┘ ┴ ┴ └┘ └┘
src └─────┘└────────────┘┴ ┴ └─────────────┘┴ ┴ └─┘ └───┘┴ └─────────────┘┴ ┴ └─┘ ┴└┘┴ └───
typ └─────┘└────────────┘┴ ┴ └─────────────┘┴ ┴ └─┘ └───┘┴ └─────────────┘┴┴┴┴└─┘ ┴└┘┴└┘└───
doc └─────┘└────────────┘┴ ┴ └─────────────┘┴ ┴ └─┘ └───┘┴ └─────────────┘┴ ┴ └─┘ ┴└┘┴ └───
txt └─────┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ └───
par └─────┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ └───
pid └───┘└┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ └───
st ─────────────────────────────────────────────────────────────────────────────────────────────────
302 Hausdorff_dist_optimal_le_HD _ _ (candidates_b_of_candidates_mem F Fgood),
id └──────────────────────────┘ └────────────────────────────┘ ┴ └───┘
src ─────┘└──────────────────────────┘└───┘ └────────────────────────────┘┴ ┴ ┴
typ ─────┘└──────────────────────────┘└───┘ └────────────────────────────┘┴┴┴└───┘┴
doc ─────┘└──────────────────────────┘└───┘ ┴ ┴ ┴
txt ─────┘ └───┘ ┴ ┴ ┴
par ─────┘ └───┘ ┴ ┴ ┴
pid ─────┘ └───┘ ┴ ┴ ┴
st ──────────────────────────────────────────────────────────────────────────────┘└─
303 refine le_trans this (le_of_forall_le_of_dense (λr hr, _)),
id └──────┘ └──┘ └──────────────────────┘
src └─────┘└──────┘┴ ┴ └──────────────────────┘┴ └───────┘
typ └─────┘└──────┘┴└──┘┴ └──────────────────────┘┴ └───────┘
doc └─────┘ ┴ ┴ ┴ └───────┘
txt └─────┘ ┴ ┴ ┴ └───────┘
par └─────┘ ┴ ┴ ┴ └───────┘
pid ┴ ┴ ┴ ┴ └───────┘
st ─────────────────────────────────────────────────────────────┘└─
304 have I1 : ∀x : α, infi (λy:β, Fb (inl x, inr y)) ≤ r,
id ┴ └──┘ ┴ └┘ ┴└─┘ └─┘ ┴
src └────────┘ └──┘ ┴└──┘┴ └┘ └┘ ┴┴└─┘┴ └┘└─┘┴ └─┘ ┴
typ └────────┘ └──┘┴ ┴└──┘┴ └┘┴└┘└┘┴┴└─┘┴ └┘└─┘┴ └─┘ ┴┴
doc └────────┘ └──┘ ┴└──┘┴ └┘ └┘ ┴ ┴ └┘ ┴ └─┘ ┴
txt └────────┘ └──┘ ┴ ┴ └┘ └┘ ┴ ┴ └┘ ┴ └─┘ ┴
par └────────┘ └──┘ ┴ ┴ └┘ └┘ ┴ ┴ └┘ ┴ └─┘ ┴
pid └─────┘└─┘ └──┘ ┴ ┴ └┘ └┘ ┴ ┴ └┘ ┴ └─┘ ┴
st ───────────────────────────────────────────────────────┘└─
305 { assume x,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid └──────┘
st ─────┘└──────┘└─
306 have : f (inl x) ∈ p.val, by { rw [← Φrange], apply mem_range_self },
id ┴ └─┘ ┴ └───┘ └────┘ └────────────┘
src └─────┘ ┴ └─┘┴ └┘ ┴└───┘ └────┘ ┴ └────┘└────────────┘┴
typ └─────┘┴┴ └─┘┴┴└┘ ┴└───┘ └────┘└────┘┴ └────┘└────────────┘┴
doc └─────┘ ┴ ┴ └┘ ┴ └────┘ ┴ └────┘ ┴
txt └─────┘ ┴ ┴ └┘ ┴ └────┘ ┴ └────┘ ┴
par └─────┘ ┴ ┴ └┘ ┴ └────┘ ┴ └────┘ ┴
pid └───┘└┘ ┴ ┴ └┘ ┴ └──┘ ┴ ┴ ┴
st ─────────────────────────────┘ ┴└───────────┘└──────────────────────┘└┘└
307 rcases exists_dist_lt_of_Hausdorff_dist_lt this hr
id └─────────────────────────────────┘ └──┘ └┘
src └─────┘└─────────────────────────────────┘┴ ┴ └
typ └─────┘└─────────────────────────────────┘┴└──┘┴└┘└
doc └─────┘└─────────────────────────────────┘┴ ┴ └
txt └─────┘ ┴ ┴ └
par └─────┘ ┴ ┴ └
pid ┴ ┴ ┴ └
st ─────────────────────────────────────────────────────────
308 (Hausdorff_edist_ne_top_of_nonempty_of_bounded p.2.1 q.2.1 p.2.2.bounded q.2.2.bounded)
id └───────────────────────────────────────────┘ ┴ ┴
src ───────┘ └───────────────────────────────────────────┘┴ └───┘ └───┘ └───────────┘ └─────────────
typ ───────┘ └───────────────────────────────────────────┘┴ └───┘ └───┘┴└───────────┘┴└─────────────
doc ───────┘ └───────────────────────────────────────────┘┴ └───┘ └───┘ └───────────┘ └─────────────
txt ───────┘ ┴ └───┘ └───┘ └───────────┘ └─────────────
par ───────┘ ┴ └───┘ └───┘ └───────────┘ └─────────────
pid ───────┘ ┴ └───┘ └───┘ └───────────┘ └─────────────
st ────────────────────────────────────────────────────────────────────────────────────────────────
309 with ⟨z, zq, hz⟩,
src ───────────────────────┘
typ ───────────────────────┘
doc ───────────────────────┘
txt ───────────────────────┘
par ───────────────────────┘
pid ───────────────────────┘
st ───────────────────────┘└─
310 have : z ∈ range Ψ, by rwa [← Ψrange] at zq,
id ┴ └───┘ ┴ └────┘
src └─────┘ ┴ ┴└───┘┴ └─────┘ └─────┘
typ └─────┘┴┴ ┴└───┘┴┴ └─────┘└────┘└─────┘
doc └─────┘ ┴ ┴└───┘┴ └─────┘ └─────┘
txt └─────┘ ┴ ┴ ┴ └─────┘ └─────┘
par └─────┘ ┴ ┴ ┴ └─────┘ └─────┘
pid └───┘└┘ ┴ ┴ ┴ └──┘ ┴└────┘
st ───────────────────────┘ └──────┘┴ └─
311 rcases mem_range.1 this with ⟨y, hy⟩,
id └───────┘ └──┘
src └─────┘└───────┘└─┘ └───────────┘
typ └─────┘└───────┘└─┘└──┘└───────────┘
doc └─────┘ └─┘ └───────────┘
txt └─────┘ └─┘ └───────────┘
par └─────┘ └─┘ └───────────┘
pid ┴ └─┘ └───────────┘
st ─────────────────────────────────────────┘└─
312 calc infi (λy:β, Fb (inl x, inr y)) ≤ Fb (inl x, inr y) :
id └──┘ └──┘ ┴ └┘ └─┘ ┴ └─┘ ┴
src └──┘ └──┘ └─┘ └─┘
typ └──┘ └──┘ ┴ └┘ └─┘ ┴ └─┘ ┴
doc └──┘ └──┘
st ────────────────────────────────────────────────────────────────
313 cinfi_le (by simpa using HD_below_aux1 0)
id └──────┘ └───────────┘
src └──────┘ └──────────┘└───────────┘└┘
typ └──────┘ └──────────┘└───────────┘└┘
doc └──────┘ └──────────┘ └┘
txt └──────────┘ └┘
par └──────────┘ └┘
pid ┴└────┘ ┴┴
st ─────────────────────┘└──────────────────────────┘└─
314 ... = dist (Φ x) (Ψ y) : rfl
id └──┘ ┴ ┴ └─┘
src └──┘ └─┘
typ └──┘ ┴ ┴ └─┘
st ─────────────────────────────────────
315 ... = dist (f (inl x)) z : by rw hy
id ┴ ┴ └┘
src └─┘ └
typ ┴ ┴ └─┘└┘└
doc └─┘ └
txt └─┘ └
par └─┘ └
pid ┴ └
st ────────────────────────────────────┘└──────
316 ... ≤ r : le_of_lt hz },
id ┴ └──────┘ └┘
src ───────┘ └──────┘
typ ───────┘ ┴ └──────┘ └┘
doc ───────┘
txt ───────┘
par ───────┘
pid ───────┘
st ───────┘└───────────────────┘└─┘└
317 have I2 : ∀y : β, infi (λx:α, Fb (inl x, inr y)) ≤ r,
id ┴ └──┘ ┴ └┘ ┴└─┘ └─┘ ┴
src └────────┘ └──┘ ┴└──┘┴ └┘ └┘ ┴┴└─┘┴ └┘└─┘┴ └─┘ ┴
typ └────────┘ └──┘┴ ┴└──┘┴ └┘┴└┘└┘┴┴└─┘┴ └┘└─┘┴ └─┘ ┴┴
doc └────────┘ └──┘ ┴└──┘┴ └┘ └┘ ┴ ┴ └┘ ┴ └─┘ ┴
txt └────────┘ └──┘ ┴ ┴ └┘ └┘ ┴ ┴ └┘ ┴ └─┘ ┴
par └────────┘ └──┘ ┴ ┴ └┘ └┘ ┴ ┴ └┘ ┴ └─┘ ┴
pid └─────┘└─┘ └──┘ ┴ ┴ └┘ └┘ ┴ ┴ └┘ ┴ └─┘ ┴
st ───────────────────────────────────────────────────────┘└─
318 { assume y,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid └──────┘
st ─────┘└──────┘└─
319 have : f (inr y) ∈ q.val, by { rw [← Ψrange], apply mem_range_self },
id ┴ └─┘ ┴ └───┘ └────┘ └────────────┘
src └─────┘ ┴ └─┘┴ └┘ ┴└───┘ └────┘ ┴ └────┘└────────────┘┴
typ └─────┘┴┴ └─┘┴┴└┘ ┴└───┘ └────┘└────┘┴ └────┘└────────────┘┴
doc └─────┘ ┴ ┴ └┘ ┴ └────┘ ┴ └────┘ ┴
txt └─────┘ ┴ ┴ └┘ ┴ └────┘ ┴ └────┘ ┴
par └─────┘ ┴ ┴ └┘ ┴ └────┘ ┴ └────┘ ┴
pid └───┘└┘ ┴ ┴ └┘ ┴ └──┘ ┴ ┴ ┴
st ─────────────────────────────┘ ┴└───────────┘└──────────────────────┘└┘└
320 rcases exists_dist_lt_of_Hausdorff_dist_lt' this hr
id └──────────────────────────────────┘ └──┘ └┘
src └─────┘└──────────────────────────────────┘┴ ┴ └
typ └─────┘└──────────────────────────────────┘┴└──┘┴└┘└
doc └─────┘└──────────────────────────────────┘┴ ┴ └
txt └─────┘ ┴ ┴ └
par └─────┘ ┴ ┴ └
pid ┴ ┴ ┴ └
st ──────────────────────────────────────────────────────────
321 (Hausdorff_edist_ne_top_of_nonempty_of_bounded p.2.1 q.2.1 p.2.2.bounded q.2.2.bounded)
id └───────────────────────────────────────────┘ ┴ ┴
src ───────┘ └───────────────────────────────────────────┘┴ └───┘ └───┘ └───────────┘ └─────────────
typ ───────┘ └───────────────────────────────────────────┘┴ └───┘ └───┘┴└───────────┘┴└─────────────
doc ───────┘ └───────────────────────────────────────────┘┴ └───┘ └───┘ └───────────┘ └─────────────
txt ───────┘ ┴ └───┘ └───┘ └───────────┘ └─────────────
par ───────┘ ┴ └───┘ └───┘ └───────────┘ └─────────────
pid ───────┘ ┴ └───┘ └───┘ └───────────┘ └─────────────
st ────────────────────────────────────────────────────────────────────────────────────────────────
322 with ⟨z, zq, hz⟩,
src ───────────────────────┘
typ ───────────────────────┘
doc ───────────────────────┘
txt ───────────────────────┘
par ───────────────────────┘
pid ───────────────────────┘
st ───────────────────────┘└─
323 have : z ∈ range Φ, by rwa [← Φrange] at zq,
id ┴ └───┘ ┴ └────┘
src └─────┘ ┴ ┴└───┘┴ └─────┘ └─────┘
typ └─────┘┴┴ ┴└───┘┴┴ └─────┘└────┘└─────┘
doc └─────┘ ┴ ┴└───┘┴ └─────┘ └─────┘
txt └─────┘ ┴ ┴ ┴ └─────┘ └─────┘
par └─────┘ ┴ ┴ ┴ └─────┘ └─────┘
pid └───┘└┘ ┴ ┴ ┴ └──┘ ┴└────┘
st ───────────────────────┘ └──────┘┴ └─
324 rcases mem_range.1 this with ⟨x, hx⟩,
id └───────┘ └──┘
src └─────┘└───────┘└─┘ └───────────┘
typ └─────┘└───────┘└─┘└──┘└───────────┘
doc └─────┘ └─┘ └───────────┘
txt └─────┘ └─┘ └───────────┘
par └─────┘ └─┘ └───────────┘
pid ┴ └─┘ └───────────┘
st ─────────────────────────────────────────┘└─
325 calc infi (λx:α, Fb (inl x, inr y)) ≤ Fb (inl x, inr y) :
id └──┘ └──┘ ┴ └┘ └─┘ ┴ └─┘ ┴
src └──┘ └──┘ └─┘ └─┘
typ └──┘ └──┘ ┴ └┘ └─┘ ┴ └─┘ ┴
doc └──┘ └──┘
st ────────────────────────────────────────────────────────────────
326 cinfi_le (by simpa using HD_below_aux2 0)
id └──────┘ └───────────┘
src └──────┘ └──────────┘└───────────┘└┘
typ └──────┘ └──────────┘└───────────┘└┘
doc └──────┘ └──────────┘ └┘
txt └──────────┘ └┘
par └──────────┘ └┘
pid ┴└────┘ ┴┴
st ─────────────────────┘└──────────────────────────┘└─
327 ... = dist (Φ x) (Ψ y) : rfl
id └──┘ ┴ ┴ └─┘
src └──┘ └─┘
typ └──┘ ┴ ┴ └─┘
st ─────────────────────────────────────
328 ... = dist z (f (inr y)) : by rw hx
id ┴ ┴ └┘
src └─┘ └
typ ┴ ┴ └─┘└┘└
doc └─┘ └
txt └─┘ └
par └─┘ └
pid ┴ └
st ────────────────────────────────────┘└──────
329 ... ≤ r : le_of_lt hz },
id ┴ └──────┘ └┘
src ───────┘ └──────┘
typ ───────┘ ┴ └──────┘ └┘
doc ───────┘
txt ───────┘
par ───────┘
pid ───────┘
st ───────┘└───────────────────┘└─┘└
330 simp [HD, csupr_le I1, csupr_le I2] },
id └┘ └──────┘ └┘ └──────┘ └┘
src └────┘└┘└┘└──────┘┴ └┘└──────┘┴ └┘
typ └────┘└┘└┘└──────┘┴└┘└┘└──────┘┴└┘└┘
doc └────┘└┘└┘└──────┘┴ └┘└──────┘┴ └┘
txt └────┘ └┘ ┴ └┘ ┴ └┘
par └────┘ └┘ ┴ └┘ ┴ └┘
pid ┴┴ └┘ ┴ └┘ ┴ ┴┴
st ───────────────────────────────────────┘└┘└
331 /- Get the same inequality for any coupling. If the coupling is quite good, the desired
st ──────────────────────────────────────────────────────────────────────────────────────────
332 inequality has been proved above. If it is bad, then the inequality is obvious. -/
st ─────────────────────────────────────────────────────────────────────────────────────
333 have B : ∀p q : nonempty_compacts (ℓ_infty_ℝ), ⟦p⟧ = to_GH_space α → ⟦q⟧ = to_GH_space β →
id └───────────────┘ └───────┘ └─────────┘
src └───────┘ └────┘└───────────────┘┴ └───────┘┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴└─────────┘┴ ┴ └
typ └───────┘ └────┘└───────────────┘┴ └───────┘┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴└─────────┘┴ ┴ └
doc └───────┘ └────┘└───────────────┘┴ └───────┘┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴└─────────┘┴ ┴ └
txt └───────┘ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └
par └───────┘ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └
pid └────┘└─┘ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └
st ─────────────────────────────────────────────────────────────────────────────────────────────
334 Hausdorff_dist (range (optimal_GH_injl α β)) (range (optimal_GH_injr α β)) ≤ Hausdorff_dist (p.val) (q.val),
id └─────────────┘ └───┘ └─────────────┘ ┴ ┴ └────────────┘
src ───────┘ ┴ ┴ └─────────────┘┴ ┴ └─┘ └───┘┴ └─────────────┘┴ ┴ └─┘ ┴└────────────┘┴ └┘ ┴
typ ───────┘ ┴ ┴ └─────────────┘┴ ┴ └─┘ └───┘┴ └─────────────┘┴┴┴┴└─┘ ┴└────────────┘┴ └┘ ┴
doc ───────┘ ┴ ┴ └─────────────┘┴ ┴ └─┘ └───┘┴ └─────────────┘┴ ┴ └─┘ ┴└────────────┘┴ └┘ ┴
txt ───────┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ └┘ ┴
par ───────┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ └┘ ┴
pid ───────┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ └┘ ┴
st ──────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘└─
335 { assume p q hp hq,
src └──────────────┘
typ └──────────────┘
doc └──────────────┘
txt └──────────────┘
par └──────────────┘
pid └──────────────┘
st ───┘└──────────────┘└─
336 by_cases h : Hausdorff_dist (p.val) (q.val) < diam (univ : set α) + 1 + diam (univ : set β),
id └────────────┘ └───┘ └───┘ ┴ └──┘ └──┘ └─┘ ┴
src └───────┘ └─┘└────────────┘┴ └───┘└┘ └───┘└┘ ┴ ┴ └─┘ ┴ └┘ └─┘ ┴└──┘┴ └──┘└─┘└─┘┴ ┴
typ └───────┘ └─┘└────────────┘┴ └───┘└┘ └───┘└┘ ┴ ┴ └─┘ ┴┴└┘ └─┘ ┴└──┘┴ └──┘└─┘└─┘┴┴┴
doc └───────┘ └─┘└────────────┘┴ └┘ └┘ ┴ ┴ └─┘ ┴ └┘ └─┘ ┴└──┘┴ └─┘ ┴ ┴
txt └───────┘ └─┘ ┴ └┘ └┘ ┴ ┴ └─┘ ┴ └┘ └─┘ ┴ ┴ └─┘ ┴ ┴
par └───────┘ └─┘ ┴ └┘ └┘ ┴ ┴ └─┘ ┴ └┘ └─┘ ┴ ┴ └─┘ ┴ ┴
pid ┴ └─┘ ┴ └┘ └┘ ┴ ┴ └─┘ ┴ └┘ └─┘ ┴ ┴ └─┘ ┴ ┴
st ──────────────────────────────────────────────────────────────────────────────────────────────┘└─
337 { exact A p q hp hq h },
id ┴ ┴ ┴ └┘ └┘ ┴
src └────┘ ┴ ┴ ┴ ┴ ┴ ┴
typ └────┘┴┴┴┴┴┴└┘┴└┘┴┴┴
doc └────┘ ┴ ┴ ┴ ┴ ┴ ┴
txt └────┘ ┴ ┴ ┴ ┴ ┴ ┴
par └────┘ ┴ ┴ ┴ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴ ┴ ┴ ┴
st ─────┘└──────────────────┘└┘└
338 { calc Hausdorff_dist (range (optimal_GH_injl α β)) (range (optimal_GH_injr α β)) ≤ HD (candidates_b_dist α β) :
id └──┘ └─────────────┘ └───┘ └─────────────┘ └┘ └───────────────┘ ┴ ┴
src └──┘ └─────────────┘ └───┘ └─────────────┘ └┘ └───────────────┘
typ └──┘ └─────────────┘ └───┘ └─────────────┘ └┘ └───────────────┘ ┴ ┴
doc └──┘ └─────────────┘ └───┘ └─────────────┘ └┘
st ─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────
339 Hausdorff_dist_optimal_le_HD _ _ (candidates_b_dist_mem_candidates_b)
id └──────────────────────────┘ └────────────────────────────────┘
src └──────────────────────────┘ └────────────────────────────────┘
typ └──────────────────────────┘ └────────────────────────────────┘
doc └──────────────────────────┘
st ───────────────────────────────────────────────────────────────────────────────────
340 ... ≤ diam (univ : set α) + 1 + diam (univ : set β) : HD_candidates_b_dist_le
id └──┘ └──┘ └─┘ └─────────────────────┘
src └──┘ └──┘ └─┘ └─────────────────────┘
typ └──┘ └──┘ └─┘ └─────────────────────┘
doc └──┘ └─────────────────────┘
st ─────────────────────────────────────────────────────────────────────────────────────────
341 ... ≤ Hausdorff_dist (p.val) (q.val) : not_lt.1 h } },
id └────────────┘ └───┘ └───┘ └────┘┴ ┴
src └────────────┘ └───┘ └───┘ └────┘┴
typ └────────────┘ └───┘ └───┘ └────┘┴ ┴
doc └────────────┘
st ───────────────────────────────────────────────────────────┘└───┘└
342 refine le_antisymm _ _,
id └─────────┘
src └─────┘└─────────┘└──┘
typ └─────┘└─────────┘└──┘
doc └─────┘ └──┘
txt └─────┘ └──┘
par └─────┘ └──┘
pid ┴ └──┘
st ───────────────────────┘└─
343 { apply le_cInf,
id └─────┘
src └────┘└─────┘
typ └────┘└─────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ───┘└───────────┘
344 { refine (set.nonempty.prod _ _).image _; exact ⟨_, rfl⟩ },
st └┘
345 { rintro b ⟨⟨p, q⟩, ⟨hp, hq⟩, rfl⟩,
346 exact B p q hp hq } },
st └──┘
347 { exact GH_dist_le_Hausdorff_dist (isometry_optimal_GH_injl α β) (isometry_optimal_GH_injr α β) }
id ┴ ┴
typ ┴ ┴
st └─
348 end
st ──┘
349
350 /-- The Gromov-Hausdorff distance can also be realized by a coupling in `ℓ^∞(ℝ)`, by embedding
351 the optimal coupling through its Kuratowski embedding. -/
352 theorem GH_dist_eq_Hausdorff_dist (α : Type u) [metric_space α] [compact_space α] [nonempty α]
id └──┘ └──┘ ┴ ┴ └──┘ └┘ ┴
src └──┘ └──┘ └──┘ └┘
typ └──┘ └──┘ ┴ ┴ └──┘ └┘ ┴
doc └──┘ └──┘
353 (β : Type v) [metric_space β] [compact_space β] [nonempty β] :
id ┴ └──┘ └─┘ ┴ ┴ └──┘ └┘ ┴
src ┴ └──┘ └─┘ └──┘ └┘
typ ┴ └──┘ └─┘ ┴ ┴ └──┘ └┘ ┴
doc ┴ └──┘ └─┘
354 ∃Φ : α → ℓ_infty_ℝ, ∃Ψ : β → ℓ_infty_ℝ, isometry Φ ∧ isometry Ψ ∧
id ┴ └───────┘ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴
src └───────┘ └───────┘ ┴ ┴
typ ┴ └───────┘ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴
doc └───────┘ └───────┘
355 GH_dist α β = Hausdorff_dist (range Φ) (range Ψ) :=
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
356 begin
357 let F := Kuratowski_embedding (optimal_GH_coupling α β),
id ┴ ┴
typ ┴ ┴
358 let Φ := F ∘ optimal_GH_injl α β,
id ┴ ┴
typ ┴ ┴
359 let Ψ := F ∘ optimal_GH_injr α β,
id ┴ ┴
typ ┴ ┴
360 refine ⟨Φ, Ψ, _, _, _⟩,
id ┴ ┴
typ ┴ ┴
361 { exact (Kuratowski_embedding.isometry _).comp (isometry_optimal_GH_injl α β) },
id ┴ ┴
typ ┴ ┴
st └┘
362 { exact (Kuratowski_embedding.isometry _).comp (isometry_optimal_GH_injr α β) },
id ┴ ┴
typ ┴ ┴
st └┘
363 { rw [← image_univ, ← image_univ, image_comp F, image_univ, image_comp F (optimal_GH_injr α β),
id ┴ ┴
typ ┴ ┴
364 image_univ, ← Hausdorff_dist_optimal],
365 exact (Hausdorff_dist_image (Kuratowski_embedding.isometry _)).symm },
st └┘
366 end
st └─┘
367
368 -- without the next two lines, `{ exact closed_of_compact (range Φ) hΦ }` in the next
369 -- proof is very slow, as the `t2_space` instance is very hard to find
370 local attribute [instance, priority 10] order_topology.t2_space
id └─────────────────────┘
src └─────────────────────┘
typ └─────────────────────┘
371 local attribute [instance, priority 10] order_closed_topology.to_t2_space
id └───────────────────────────────┘
src └───────────────────────────────┘
typ └───────────────────────────────┘
372
373 /-- The Gromov-Hausdorff distance defines a genuine distance on the Gromov-Hausdorff space. -/
374 instance GH_space_metric_space : metric_space GH_space :=
id └──────────┘ └──────┘
src └──────────┘ └──────┘
typ └──────────┘ └──────┘
doc └──────────┘ └──────┘
375 { dist_self := λx, begin
id ┴ ┴
src ┴
typ ┴ ┴
st └─────
376 rcases exists_rep x with ⟨y, hy⟩,
id └────────┘ ┴
src └─────┘└────────┘┴ └───────────┘
typ └─────┘└────────┘┴┴└───────────┘
doc └─────┘ ┴ └───────────┘
txt └─────┘ ┴ └───────────┘
par └─────┘ ┴ └───────────┘
pid ┴ ┴ └───────────┘
st ───────────────────────────────────┘└─
377 refine le_antisymm _ _,
id └─────────┘
src └─────┘└─────────┘└──┘
typ └─────┘└─────────┘└──┘
doc └─────┘ └──┘
txt └─────┘ └──┘
par └─────┘ └──┘
pid ┴ └──┘
st ─────────────────────────┘└─
378 { apply cInf_le,
id └─────┘
src └────┘└─────┘
typ └────┘└─────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ─────┘└───────────┘
379 { exact ⟨0, by { rintro b ⟨⟨u, v⟩, ⟨hu, hv⟩, rfl⟩, exact Hausdorff_dist_nonneg } ⟩},
src └┘
typ └┘
doc └┘
txt └┘
par └┘
st └┘ └┘ └┘
380 { simp, existsi [y, y], simpa } },
st └──┘
381 { apply le_cInf,
382 { exact (nonempty.prod ⟨y, hy⟩ ⟨y, hy⟩).image _ },
st └┘
383 { rintro b ⟨⟨u, v⟩, ⟨hu, hv⟩, rfl⟩, exact Hausdorff_dist_nonneg } },
st └──┘
384 end,
st └─┘
385 dist_comm := λx y, begin
id ┴ ┴
typ ┴ ┴
386 have A : (λ (p : nonempty_compacts ℓ_infty_ℝ × nonempty_compacts ℓ_infty_ℝ),
387 Hausdorff_dist ((p.fst).val) ((p.snd).val)) '' (set.prod {a | ⟦a⟧ = x} {b | ⟦b⟧ = y})
388 = ((λ (p : nonempty_compacts ℓ_infty_ℝ × nonempty_compacts ℓ_infty_ℝ),
id └───────┘
src └───────┘
typ └───────┘
doc └───────┘
389 Hausdorff_dist ((p.fst).val) ((p.snd).val)) ∘ prod.swap) '' (set.prod {a | ⟦a⟧ = x} {b | ⟦b⟧ = y}) :=
id ┴ ┴
typ ┴ ┴
390 by { congr, funext, simp, rw Hausdorff_dist_comm },
st └┘
391 simp only [dist, A, image_comp, prod.swap, image_swap_prod],
392 end,
st └─┘
393 eq_of_dist_eq_zero := λx y hxy, begin
id ┴ ┴
typ ┴ ┴
394 /- To show that two spaces at zero distance are isometric, we argue that the distance
395 is realized by some coupling. In this coupling, the two spaces are at zero Hausdorff distance,
396 i.e., they coincide. Therefore, the original spaces are isometric. -/
397 rcases GH_dist_eq_Hausdorff_dist x.rep y.rep with ⟨Φ, Ψ, Φisom, Ψisom, DΦΨ⟩,
id └───┘ └───┘
src └───┘ └───┘
typ └───┘ └───┘
doc └───┘ └───┘
398 rw [← dist_GH_dist, hxy] at DΦΨ,
399 have : range Φ = range Ψ,
id ┴ ┴
typ ┴ ┴
400 { have hΦ : compact (range Φ) := compact_range Φisom.continuous,
id ┴
typ ┴
401 have hΨ : compact (range Ψ) := compact_range Ψisom.continuous,
id ┴
typ ┴
402 apply (Hausdorff_dist_zero_iff_eq_of_closed _ _ _).1 (DΦΨ.symm),
403 { exact closed_of_compact (range Φ) hΦ },
id ┴
typ ┴
st └┘
404 { exact closed_of_compact (range Ψ) hΨ },
id ┴
typ ┴
st └┘
405 { exact Hausdorff_edist_ne_top_of_nonempty_of_bounded (range_nonempty _)
406 (range_nonempty _) hΦ.bounded hΨ.bounded } },
st └──┘
407 have T : ((range Ψ) ≃ᵢ y.rep) = ((range Φ) ≃ᵢ y.rep), by rw this,
id ┴ ┴ └───┘
src └───┘
typ ┴ ┴ └───┘
doc └───┘
408 have eΨ := cast T Ψisom.isometric_on_range.symm,
409 have e := Φisom.isometric_on_range.trans eΨ,
410 rw [← x.to_GH_space_rep, ← y.to_GH_space_rep, to_GH_space_eq_to_GH_space_iff_isometric],
411 exact ⟨e⟩
412 end,
st └─┘
413 dist_triangle := λx y z, begin
id ┴ ┴ ┴
typ ┴ ┴ ┴
414 /- To show the triangular inequality between `X`, `Y` and `Z`, realize an optimal coupling
415 between `X` and `Y` in a space `γ1`, and an optimal coupling between `Y`and `Z` in a space `γ2`.
416 Then, glue these metric spaces along `Y`. We get a new space `γ` in which `X` and `Y` are
417 optimally coupled, as well as `Y` and `Z`. Apply the triangle inequality for the Hausdorff
418 distance in `γ` to conclude. -/
419 let X := x.rep,
id └───┘
src └───┘
typ └───┘
doc └───┘
420 let Y := y.rep,
id └───┘
src └───┘
typ └───┘
doc └───┘
421 let Z := z.rep,
id └───┘
src └───┘
typ └───┘
doc └───┘
422 let γ1 := optimal_GH_coupling X Y,
id ┴
typ ┴
423 let γ2 := optimal_GH_coupling Y Z,
id ┴ ┴
typ ┴ ┴
424 let Φ : Y → γ1 := optimal_GH_injr X Y,
id ┴ └┘ ┴ ┴
typ ┴ └┘ ┴ ┴
425 have hΦ : isometry Φ := isometry_optimal_GH_injr X Y,
id ┴ ┴ ┴
typ ┴ ┴ ┴
426 let Ψ : Y → γ2 := optimal_GH_injl Y Z,
id ┴ └┘ ┴ ┴
typ ┴ └┘ ┴ ┴
427 have hΨ : isometry Ψ := isometry_optimal_GH_injl Y Z,
id ┴ ┴ ┴
typ ┴ ┴ ┴
428 let γ := glue_space hΦ hΨ,
429 letI : metric_space γ := metric.metric_space_glue_space hΦ hΨ,
id └──────────┘ ┴
src └──────────┘
typ └──────────┘ ┴
doc └──────────┘
430 have Comm : (to_glue_l hΦ hΨ) ∘ (optimal_GH_injr X Y) = (to_glue_r hΦ hΨ) ∘ (optimal_GH_injl Y Z) :=
id ┴ ┴ ┴
typ ┴ ┴ ┴
431 to_glue_commute hΦ hΨ,
432 calc dist x z = dist (to_GH_space X) (to_GH_space Z) :
433 by rw [x.to_GH_space_rep, z.to_GH_space_rep]
st ┴
434 ... ≤ Hausdorff_dist (range ((to_glue_l hΦ hΨ) ∘ (optimal_GH_injl X Y)))
435 (range ((to_glue_r hΦ hΨ) ∘ (optimal_GH_injr Y Z))) :
436 GH_dist_le_Hausdorff_dist
437 ((to_glue_l_isometry hΦ hΨ).comp (isometry_optimal_GH_injl X Y))
id ┴
typ ┴
438 ((to_glue_r_isometry hΦ hΨ).comp (isometry_optimal_GH_injr Y Z))
id ┴ ┴
typ ┴ ┴
439 ... ≤ Hausdorff_dist (range ((to_glue_l hΦ hΨ) ∘ (optimal_GH_injl X Y)))
440 (range ((to_glue_l hΦ hΨ) ∘ (optimal_GH_injr X Y)))
441 + Hausdorff_dist (range ((to_glue_l hΦ hΨ) ∘ (optimal_GH_injr X Y)))
442 (range ((to_glue_r hΦ hΨ) ∘ (optimal_GH_injr Y Z))) :
443 begin
444 refine Hausdorff_dist_triangle (Hausdorff_edist_ne_top_of_nonempty_of_bounded
445 (range_nonempty _) (range_nonempty _) _ _),
446 { exact (compact_range (isometry.continuous ((to_glue_l_isometry hΦ hΨ).comp
447 (isometry_optimal_GH_injl X Y)))).bounded },
id ┴ ┴
typ ┴ ┴
st └┘
448 { exact (compact_range (isometry.continuous ((to_glue_l_isometry hΦ hΨ).comp
449 (isometry_optimal_GH_injr X Y)))).bounded }
id ┴ ┴
typ ┴ ┴
st └┘
450 end
st └─┘
451 ... = Hausdorff_dist ((to_glue_l hΦ hΨ) '' (range (optimal_GH_injl X Y)))
452 ((to_glue_l hΦ hΨ) '' (range (optimal_GH_injr X Y)))
453 + Hausdorff_dist ((to_glue_r hΦ hΨ) '' (range (optimal_GH_injl Y Z)))
454 ((to_glue_r hΦ hΨ) '' (range (optimal_GH_injr Y Z))) :
455 by simp only [eq.symm range_comp, Comm, eq_self_iff_true, add_right_inj]
456 ... = Hausdorff_dist (range (optimal_GH_injl X Y))
457 (range (optimal_GH_injr X Y))
458 + Hausdorff_dist (range (optimal_GH_injl Y Z))
459 (range (optimal_GH_injr Y Z)) :
460 by rw [Hausdorff_dist_image (to_glue_l_isometry hΦ hΨ),
461 Hausdorff_dist_image (to_glue_r_isometry hΦ hΨ)]
st ┴
462 ... = dist (to_GH_space X) (to_GH_space Y) + dist (to_GH_space Y) (to_GH_space Z) :
463 by rw [Hausdorff_dist_optimal, Hausdorff_dist_optimal, GH_dist, GH_dist]
st ┴
464 ... = dist x y + dist y z:
id ┴ ┴ ┴
typ ┴ ┴ ┴
465 by rw [x.to_GH_space_rep, y.to_GH_space_rep, z.to_GH_space_rep]
st ┴
466 end }
st └─┘
467
468 end GH_space --section
469 end Gromov_Hausdorff
470
471 /-- In particular, nonempty compacts of a metric space map to `GH_space`. We register this
472 in the topological_space namespace to take advantage of the notation `p.to_GH_space`. -/
473 definition topological_space.nonempty_compacts.to_GH_space {α : Type u} [metric_space α]
id └──┘ └──┘ ┴
src └──┘ └──┘
typ └──┘ └──┘ ┴
doc └──┘ └──┘
474 (p : nonempty_compacts α) : Gromov_Hausdorff.GH_space := Gromov_Hausdorff.to_GH_space p.val
id ┴ └───────────────────────┘
src └───────────────────────┘
typ ┴ └───────────────────────┘
doc └───────────────────────┘
475
476 open topological_space
477
478 namespace Gromov_Hausdorff
479
480 section nonempty_compacts
481 variables {α : Type u} [metric_space α]
id └─────────┘
src └─────────┘
typ └─────────┘
doc └─────────┘
482
483 theorem GH_dist_le_nonempty_compacts_dist (p q : nonempty_compacts α) :
id └───────────────┘ ┴
src └───────────────┘
typ └───────────────┘ ┴
doc └───────────────┘
484 dist p.to_GH_space q.to_GH_space ≤ dist p q :=
id └──┘ ┴└──────────┘ ┴└──────────┘ ┴ └──┘ ┴ ┴
src └──┘ └──────────┘ └──────────┘ ┴ └──┘
typ └──┘ ┴└──────────┘ ┴└──────────┘ ┴ └──┘ ┴ ┴
doc └──────────┘ └──────────┘
485 begin
st └─────
486 have ha : isometry (subtype.val : p.val → α) := isometry_subtype_val,
id └──────┘ └─────────┘ └───┘ ┴ └──────────────────┘
src ┴ └──────┘ └─────────┘ └───┘ └──────────────────┘
typ ┴ └──────┘ └─────────┘ └───┘ ┴ └──────────────────┘
doc ┴ └──────┘ └──────────────────┘
txt ┴
par ┴
pid ┴
st ──┘ └──────┘ └──────────┘ └───┘ ┴ ┴ └──────────────────┘└─
487 have hb : isometry (subtype.val : q.val → α) := isometry_subtype_val,
id └──────┘ └─────────┘ └───┘ ┴ └──────────────────┘
src └──────┘ └─────────┘ └───┘ └──────────────────┘
typ └──────┘ └─────────┘ └───┘ ┴ └──────────────────┘
doc └──────┘ └──────────────────┘
st ─┘ └──────┘ └──────────┘ └───┘ ┴ ┴ └──────────────────┘
488 have A : dist p q = Hausdorff_dist p.val q.val := rfl,
489 have I : p.val = range (subtype.val : p.val → α), by simp,
490 have J : q.val = range (subtype.val : q.val → α), by simp,
491 rw [I, J] at A,
492 rw A,
493 exact GH_dist_le_Hausdorff_dist ha hb
494 end
st └─┘
495
496 lemma to_GH_space_lipschitz :
497 lipschitz_with 1 (nonempty_compacts.to_GH_space : nonempty_compacts α → GH_space) :=
id └────────────┘ └───────────────────────────┘ └───────────────┘ ┴ └──────┘
src └────────────┘ └───────────────────────────┘ └───────────────┘ └──────┘
typ └────────────┘ └───────────────────────────┘ └───────────────┘ ┴ └──────┘
doc └────────────┘ └───────────────────────────┘ └───────────────┘ └──────┘
498 lipschitz_with.one_mk GH_dist_le_nonempty_compacts_dist
id └───────────────────┘ └───────────────────────────────┘
src └───────────────────┘ └───────────────────────────────┘
typ └───────────────────┘ └───────────────────────────────┘
499
500 lemma to_GH_space_continuous :
501 continuous (nonempty_compacts.to_GH_space : nonempty_compacts α → GH_space) :=
id └────────┘ └───────────────────────────┘ └───────────────┘ ┴ └──────┘
src └────────┘ └───────────────────────────┘ └───────────────┘ └──────┘
typ └────────┘ └───────────────────────────┘ └───────────────┘ ┴ └──────┘
doc └────────┘ └───────────────────────────┘ └───────────────┘ └──────┘
502 to_GH_space_lipschitz.to_continuous
id └───────────────────┘└────────────┘
src └───────────────────┘└────────────┘
typ └───────────────────┘└────────────┘
doc └────────────┘
503
504 end nonempty_compacts
505
506 section
507 /- In this section, we show that if two metric spaces are isometric up to `ε₂`, then their
508 Gromov-Hausdorff distance is bounded by `ε₂ / 2`. More generally, if there are subsets which are
509 `ε₁`-dense and `ε₃`-dense in two spaces, and isometric up to `ε₂`, then the Gromov-Hausdorff distance
510 between the spaces is bounded by `ε₁ + ε₂/2 + ε₃`. For this, we construct a suitable coupling between
511 the two spaces, by gluing them (approximately) along the two matching subsets. -/
512
513 variables {α : Type u} [metric_space α] [compact_space α] [nonempty α]
id ┴ └──────────┘ └───────────┘ └──────┘
src └──────────┘ └───────────┘ └──────┘
typ ┴ └──────────┘ └───────────┘ └──────┘
doc └──────────┘ └───────────┘
514 {β : Type v} [metric_space β] [compact_space β] [nonempty β]
id └──────────┘ └───────────┘ └──────┘
src └──────────┘ └───────────┘ └──────┘
typ └──────────┘ └───────────┘ └──────┘
doc └──────────┘ └───────────┘
515
516 -- we want to ignore these instances in the following theorem
517 local attribute [instance, priority 10] sum.topological_space sum.uniform_space
id └───────────────────┘ └───────────────┘
src └───────────────────┘ └───────────────┘
typ └───────────────────┘ └───────────────┘
518 /-- If there are subsets which are `ε₁`-dense and `ε₃`-dense in two spaces, and
519 isometric up to `ε₂`, then the Gromov-Hausdorff distance between the spaces is bounded by
520 `ε₁ + ε₂/2 + ε₃`. -/
521 theorem GH_dist_le_of_approx_subsets {s : set α} (Φ : s → β) {ε₁ ε₂ ε₃ : ℝ}
id └─┘ ┴ ┴ ┴ ┴
src └─┘ ┴
typ └─┘ ┴ ┴ ┴ ┴
522 (hs : ∀x : α, ∃y ∈ s, dist x y ≤ ε₁) (hs' : ∀x : β, ∃y : s, dist x (Φ y) ≤ ε₃)
id ┴ ┴┴ ┴┴ └──┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴┴ └──┘ ┴ ┴ ┴ ┴ └┘
src ┴ ┴ └──┘ ┴ ┴ ┴ └──┘ ┴
typ ┴ ┴┴ ┴┴ └──┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴┴ └──┘ ┴ ┴ ┴ ┴ └┘
523 (H : ∀x y : s, abs (dist x y - dist (Φ x) (Φ y)) ≤ ε₂) :
id ┴ └─┘ └──┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ └┘
src └─┘ └──┘ ┴ └──┘ ┴
typ ┴ └─┘ └──┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ └┘
524 GH_dist α β ≤ ε₁ + ε₂ / 2 + ε₃ :=
id └─────┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴ └┘
src └─────┘ ┴ ┴ ┴ ┴
typ └─────┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴ └┘
doc └─────┘
525 begin
st └───┘
526 refine real.le_of_forall_epsilon_le (λδ δ0, _),
id ┴
typ ┴
527 rcases exists_mem_of_nonempty α with ⟨xα, _⟩,
id ┴
typ ┴
528 rcases hs xα with ⟨xs, hxs, Dxs⟩,
id └┘
typ └┘
529 have sne : s.nonempty := ⟨xs, hxs⟩,
id └┘
typ └┘
530 letI : nonempty s := sne.to_subtype,
id └──────┘ ┴
src └──────┘
typ └──────┘ ┴
531 have : 0 ≤ ε₂ := le_trans (abs_nonneg _) (H ⟨xs, hxs⟩ ⟨xs, hxs⟩),
id └┘ └┘
typ └┘ └┘
532 have : ∀ p q : s, abs (dist p q - dist (Φ p) (Φ q)) ≤ 2 * (ε₂/2 + δ) := λp q, calc
id └┘ ┴
typ └┘ ┴
533 abs (dist p q - dist (Φ p) (Φ q)) ≤ ε₂ : H p q
534 ... ≤ 2 * (ε₂/2 + δ) : by linarith,
id └┘ ┴
typ └┘ ┴
535 -- glue `α` and `β` along the almost matching subsets
536 letI : metric_space (α ⊕ β) := glue_metric_approx (λ x:s, (x:α)) (λx, Φ x) (ε₂/2 + δ) (by linarith) this,
id ┴ ┴ ┴ └┘ ┴
typ ┴ ┴ ┴ └┘ ┴
537 let Fl := @sum.inl α β,
id ┴ ┴
typ ┴ ┴
538 let Fr := @sum.inr α β,
id ┴ ┴
typ ┴ ┴
539 have Il : isometry Fl := isometry_emetric_iff_metric.2 (λx y, rfl),
id └┘ ┴ ┴
typ └┘ ┴ ┴
540 have Ir : isometry Fr := isometry_emetric_iff_metric.2 (λx y, rfl),
id └┘ ┴ ┴
typ └┘ ┴ ┴
541 /- The proof goes as follows : the `GH_dist` is bounded by the Hausdorff distance of the images in the
542 coupling, which is bounded (using the triangular inequality) by the sum of the Hausdorff distances
543 of `α` and `s` (in the coupling or, equivalently in the original space), of `s` and `Φ s`, and of
544 `Φ s` and `β` (in the coupling or, equivalently, in the original space). The first term is bounded
545 by `ε₁`, by `ε₁`-density. The third one is bounded by `ε₃`. And the middle one is bounded by `ε₂/2`
546 as in the coupling the points `x` and `Φ x` are at distance `ε₂/2` by construction of the coupling
547 (in fact `ε₂/2 + δ` where `δ` is an arbitrarily small positive constant where positivity is used
548 to ensure that the coupling is really a metric space and not a premetric space on `α ⊕ β`). -/
549 have : GH_dist α β ≤ Hausdorff_dist (range Fl) (range Fr) :=
id ┴ ┴ └┘ └┘
typ ┴ ┴ └┘ └┘
550 GH_dist_le_Hausdorff_dist Il Ir,
551 have : Hausdorff_dist (range Fl) (range Fr) ≤ Hausdorff_dist (range Fl) (Fl '' s)
552 + Hausdorff_dist (Fl '' s) (range Fr),
id ┴
typ ┴
553 { have B : bounded (range Fl) := (compact_range Il.continuous).bounded,
id └┘
typ └┘
554 exact Hausdorff_dist_triangle (Hausdorff_edist_ne_top_of_nonempty_of_bounded
555 (range_nonempty _) (sne.image _) B (B.subset (image_subset_range _ _))) },
st └┘
556 have : Hausdorff_dist (Fl '' s) (range Fr) ≤ Hausdorff_dist (Fl '' s) (Fr '' (range Φ))
id ┴
typ ┴
557 + Hausdorff_dist (Fr '' (range Φ)) (range Fr),
558 { have B : bounded (range Fr) := (compact_range Ir.continuous).bounded,
id └┘
typ └┘
559 exact Hausdorff_dist_triangle' (Hausdorff_edist_ne_top_of_nonempty_of_bounded
560 ((range_nonempty _).image _) (range_nonempty _)
561 (bounded.subset (image_subset_range _ _) B) B) },
st └┘
562 have : Hausdorff_dist (range Fl) (Fl '' s) ≤ ε₁,
id ┴ └┘
typ ┴ └┘
563 { rw [← image_univ, Hausdorff_dist_image Il],
564 have : 0 ≤ ε₁ := le_trans dist_nonneg Dxs,
id └┘ ┴
typ └┘ ┴
565 refine Hausdorff_dist_le_of_mem_dist this (λx hx, hs x)
id └──┘ ┴ └┘ └┘
typ └──┘ ┴ └┘ └┘
566 (λx hx, ⟨x, mem_univ _, by simpa⟩) },
id ┴ └┘ └──────┘
src └──────┘
typ ┴ └┘ └──────┘
st └┘
567 have : Hausdorff_dist (Fl '' s) (Fr '' (range Φ)) ≤ ε₂/2 + δ,
id └────────────┘ └┘ ┴ └┘ └───┘ ┴ └┘ ┴
src └────────────┘ └───┘
typ └────────────┘ └┘ ┴ └┘ └───┘ ┴ └┘ ┴
doc └────────────┘ └───┘
568 { refine Hausdorff_dist_le_of_mem_dist (by linarith) _ _,
569 { assume x' hx',
570 rcases (set.mem_image _ _ _).1 hx' with ⟨x, ⟨x_in_s, xx'⟩⟩,
571 rw ← xx',
572 use [Fr (Φ ⟨x, x_in_s⟩), mem_image_of_mem Fr (mem_range_self _)],
id ┴
typ ┴
573 exact le_of_eq (glue_dist_glued_points (λ x:s, (x:α)) Φ (ε₂/2 + δ) ⟨x, x_in_s⟩) },
id ┴ └┘ ┴ ┴
typ ┴ └┘ ┴ ┴
st └┘
574 { assume x' hx',
575 rcases (set.mem_image _ _ _).1 hx' with ⟨y, ⟨y_in_s', yx'⟩⟩,
576 rcases mem_range.1 y_in_s' with ⟨x, xy⟩,
577 use [Fl x, mem_image_of_mem _ x.2],
578 rw [← yx', ← xy, dist_comm],
id └┘
typ └┘
579 exact le_of_eq (glue_dist_glued_points (@subtype.val α s) Φ (ε₂/2 + δ) x) } },
id ┴ ┴ └┘ ┴
typ ┴ ┴ └┘ ┴
st └──┘
580 have : Hausdorff_dist (Fr '' (range Φ)) (range Fr) ≤ ε₃,
id └┘
typ └┘
581 { rw [← @image_univ _ _ Fr, Hausdorff_dist_image Ir],
id └┘
typ └┘
582 rcases exists_mem_of_nonempty β with ⟨xβ, _⟩,
id ┴
typ ┴
583 rcases hs' xβ with ⟨xs', Dxs'⟩,
id └┘
typ └┘
584 have : 0 ≤ ε₃ := le_trans dist_nonneg Dxs',
id └┘
typ └┘
585 refine Hausdorff_dist_le_of_mem_dist this (λx hx, ⟨x, mem_univ _, by simpa⟩) (λx _, _),
id ┴ ┴
typ ┴ ┴
586 rcases hs' x with ⟨y, Dy⟩,
id ┴
typ ┴
587 exact ⟨Φ y, mem_range_self _, Dy⟩ },
st └┘
588 linarith
589 end
st └─┘
590 end --section
591
592 /-- The Gromov-Hausdorff space is second countable. -/
593 instance second_countable : second_countable_topology GH_space :=
id └──────┘
src └──────┘
typ └──────┘
doc └──────┘
594 begin
595 refine second_countable_of_countable_discretization (λδ δpos, _),
596 let ε := (2/5) * δ,
id ┴
typ ┴
597 have εpos : 0 < ε := mul_pos (by norm_num) δpos,
id ┴
typ ┴
598 have : ∀p:GH_space, ∃s : set (p.rep), finite s ∧ (univ ⊆ (⋃x∈s, ball x ε)) :=
id └──────┘ └──┘ └──┘ ┴ ┴
src └──────┘ └──┘ └──┘
typ └──────┘ └──┘ └──┘ ┴ ┴
doc └──────┘ └──┘
599 λp, by simpa using finite_cover_balls_of_compact (@compact_univ p.rep _ _) εpos,
id ┴ └───┘
src └───┘
typ ┴ └───┘
doc └───┘
600 -- for each `p`, `s p` is a finite `ε`-dense subset of `p` (or rather the metric space
601 -- `p.rep` representing `p`)
602 choose s hs using this,
603 have : ∀p:GH_space, ∀t:set (p.rep), finite t → ∃n:ℕ, ∃e:equiv t (fin n), true,
id └──────┘ └─┘ └─┘ └──┘
src └──────┘ └─┘ └─┘ └──┘
typ └──────┘ └─┘ └─┘ └──┘
doc └──────┘
604 { assume p t ht,
605 letI : fintype t := finite.fintype ht,
id └─────┘ ┴ └┘
src └─────┘
typ └─────┘ ┴ └┘
doc └─────┘
606 rcases fintype.exists_equiv_fin t with ⟨n, hn⟩,
id ┴
typ ┴
607 rcases hn with e,
608 exact ⟨n, e, trivial⟩ },
id ┴ └─────┘
src └─────┘
typ ┴ └─────┘
st └┘
609 choose N e hne using this,
610 -- cardinality of the nice finite subset `s p` of `p.rep`, called `N p`
611 let N := λp:GH_space, N p (s p) (hs p).1,
id └──────┘
src └──────┘
typ └──────┘
doc └──────┘
612 -- equiv from `s p`, a nice finite subset of `p.rep`, to `fin (N p)`, called `E p`
613 let E := λp:GH_space, e p (s p) (hs p).1,
id └──────┘
src └──────┘
typ └──────┘
doc └──────┘
614 -- A function `F` associating to `p : GH_space` the data of all distances between points
615 -- in the `ε`-dense set `s p`.
616 let F : GH_space → Σn:ℕ, (fin n → fin n → ℤ) :=
id └──────┘ └─┘
src └──────┘ └─┘
typ └──────┘ └─┘
doc └──────┘
617 λp, ⟨N p, λa b, floor (ε⁻¹ * dist ((E p).inv_fun a) ((E p).inv_fun b))⟩,
id ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
618 refine ⟨_, by apply_instance, F, λp q hpq, _⟩,
id ┴ ┴
typ ┴ ┴
619 /- As the target space of F is countable, it suffices to show that two points
620 `p` and `q` with `F p = F q` are at distance `≤ δ`.
621 For this, we construct a map `Φ` from `s p ⊆ p.rep` (representing `p`)
622 to `q.rep` (representing `q`) which is almost an isometry on `s p`, and
623 with image `s q`. For this, we compose the identification of `s p` with `fin (N p)`
624 and the inverse of the identification of `s q` with `fin (N q)`. Together with
625 the fact that `N p = N q`, this constructs `Ψ` between `s p` and `s q`, and then
626 composing with the canonical inclusion we get `Φ`. -/
627 have Npq : N p = N q := (sigma.mk.inj_iff.1 hpq).1,
id ┴ ┴ ┴
typ ┴ ┴ ┴
628 let Ψ : s p → s q := λx, (E q).inv_fun (fin.cast Npq ((E p).to_fun x)),
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
629 let Φ : s p → q.rep := λx, Ψ x,
id ┴ └───┘
src └───┘
typ ┴ └───┘
doc └───┘
630 -- Use the almost isometry `Φ` to show that `p.rep` and `q.rep`
631 -- are within controlled Gromov-Hausdorff distance.
632 have main : GH_dist p.rep q.rep ≤ ε + ε/2 + ε,
id └───┘ └───┘ ┴
src └───┘ └───┘
typ └───┘ └───┘ ┴
doc └───┘ └───┘
633 { refine GH_dist_le_of_approx_subsets Φ _ _ _,
634 show ∀x : p.rep, ∃ (y : p.rep) (H : y ∈ s p), dist x y ≤ ε,
id └───┘ ┴ ┴
src └───┘
typ └───┘ ┴ ┴
doc └───┘
635 { -- by construction, `s p` is `ε`-dense
636 assume x,
637 have : x ∈ ⋃y∈(s p), ball y ε := (hs p).2 (mem_univ _),
id ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
638 rcases mem_bUnion_iff.1 this with ⟨y, ys, hy⟩,
639 exact ⟨y, ys, le_of_lt hy⟩ },
id ┴
typ ┴
st └┘
640 show ∀x : q.rep, ∃ (z : s p), dist x (Φ z) ≤ ε,
id └───┘ ┴ ┴
src └───┘
typ └───┘ ┴ ┴
doc └───┘
641 { -- by construction, `s q` is `ε`-dense, and it is the range of `Φ`
642 assume x,
643 have : x ∈ ⋃y∈(s q), ball y ε := (hs q).2 (mem_univ _),
id ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
644 rcases mem_bUnion_iff.1 this with ⟨y, ys, hy⟩,
645 let i := ((E q).to_fun ⟨y, ys⟩).1,
id ┴ ┴
typ ┴ ┴
646 let hi := ((E q).to_fun ⟨y, ys⟩).2,
id ┴ ┴
typ ┴ ┴
647 have ihi_eq : (⟨i, hi⟩ : fin (N q)) = (E q).to_fun ⟨y, ys⟩, by rw fin.ext_iff,
id ┴ └─┘ ┴ ┴ ┴
src └─┘
typ ┴ └─┘ ┴ ┴ ┴
648 have hiq : i < N q := hi,
id ┴ ┴ ┴
typ ┴ ┴ ┴
649 have hip : i < N p, { rwa Npq.symm at hiq },
id ┴ ┴ ┴
typ ┴ ┴ ┴
st └┘
650 let z := (E p).inv_fun ⟨i, hip⟩,
id ┴ ┴ └─┘
typ ┴ ┴ └─┘
651 use z,
652 have C1 : (E p).to_fun z = ⟨i, hip⟩ := (E p).right_inv ⟨i, hip⟩,
id ┴ ┴ └─┘ ┴ ┴ └─┘
typ ┴ ┴ └─┘ ┴ ┴ └─┘
653 have C2 : fin.cast Npq ⟨i, hip⟩ = ⟨i, hi⟩ := rfl,
id └─┘ ┴
typ └─┘ ┴
654 have C3 : (E q).inv_fun ⟨i, hi⟩ = ⟨y, ys⟩, by { rw ihi_eq, exact (E q).left_inv ⟨y, ys⟩ },
id ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
st └┘
655 have : Φ z = y :=
id ┴
typ ┴
656 by { simp only [Φ, Ψ], rw [C1, C2, C3], refl },
st └┘
657 rw this,
658 exact le_of_lt hy },
st └┘
659 show ∀x y : s p, abs (dist x y - dist (Φ x) (Φ y)) ≤ ε,
id ┴ ┴
typ ┴ ┴
660 { /- the distance between `x` and `y` is encoded in `F p`, and the distance between
661 `Φ x` and `Φ y` (two points of `s q`) is encoded in `F q`, all this up to `ε`.
662 As `F p = F q`, the distances are almost equal. -/
663 assume x y,
664 have : dist (Φ x) (Φ y) = dist (Ψ x) (Ψ y) := rfl,
665 rw this,
666 -- introduce `i`, that codes both `x` and `Φ x` in `fin (N p) = fin (N q)`
667 let i := ((E p).to_fun x).1,
id ┴
typ ┴
668 have hip : i < N p := ((E p).to_fun x).2,
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
669 have hiq : i < N q, by rwa Npq at hip,
id ┴ ┴ ┴
typ ┴ ┴ ┴
670 have i' : i = ((E q).to_fun (Ψ x)).1, by { simp [Ψ, (E q).right_inv _] },
id ┴ ┴ ┴
typ ┴ ┴ ┴
st └┘
671 -- introduce `j`, that codes both `y` and `Φ y` in `fin (N p) = fin (N q)`
672 let j := ((E p).to_fun y).1,
id ┴
typ ┴
673 have hjp : j < N p := ((E p).to_fun y).2,
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
674 have hjq : j < N q, by rwa Npq at hjp,
id ┴ ┴ ┴
typ ┴ ┴ ┴
675 have j' : j = ((E q).to_fun (Ψ y)).1, by { simp [Ψ, (E q).right_inv _] },
id ┴ ┴ ┴
typ ┴ ┴ ┴
st └┘
676 -- Express `dist x y` in terms of `F p`
677 have : (F p).2 ((E p).to_fun x) ((E p).to_fun y) = floor (ε⁻¹ * dist x y),
id ┴ ┴
typ ┴ ┴
678 by simp only [F, (E p).left_inv _],
id ┴
typ ┴
679 have Ap : (F p).2 ⟨i, hip⟩ ⟨j, hjp⟩ = floor (ε⁻¹ * dist x y),
id ┴ ┴ └─┘ ┴ └─┘ ┴
typ ┴ ┴ └─┘ ┴ └─┘ ┴
680 by { rw ← this, congr; apply (fin.ext_iff _ _).2; refl },
id └──┘
src └──┘
typ └──┘
doc └──┘
st └┘
681 -- Express `dist (Φ x) (Φ y)` in terms of `F q`
682 have : (F q).2 ((E q).to_fun (Ψ x)) ((E q).to_fun (Ψ y)) = floor (ε⁻¹ * dist (Ψ x) (Ψ y)),
id ┴ ┴
typ ┴ ┴
683 by simp only [F, (E q).left_inv _],
id ┴
typ ┴
684 have Aq : (F q).2 ⟨i, hiq⟩ ⟨j, hjq⟩ = floor (ε⁻¹ * dist (Ψ x) (Ψ y)),
id ┴ ┴ └─┘ ┴ └─┘ ┴
typ ┴ ┴ └─┘ ┴ └─┘ ┴
685 by { rw ← this, congr; apply (fin.ext_iff _ _).2; [exact i', exact j'] },
st └┘
686 -- use the equality between `F p` and `F q` to deduce that the distances have equal
687 -- integer parts
688 have : (F p).2 ⟨i, hip⟩ ⟨j, hjp⟩ = (F q).2 ⟨i, hiq⟩ ⟨j, hjq⟩,
id ┴ └─┘ └─┘ ┴ ┴ └─┘ ┴ └─┘
typ ┴ └─┘ └─┘ ┴ ┴ └─┘ ┴ └─┘
689 { -- we want to `subst hpq` where `hpq : F p = F q`, except that `subst` only works
690 -- with a constant, so replace `F q` (and everything that depends on it) by a constant `f`
691 -- then `subst`
692 revert hiq hjq,
693 change N q with (F q).1,
id ┴ ┴ ┴
typ ┴ ┴ ┴
694 generalize_hyp : F q = f at hpq ⊢,
id ┴
typ ┴
695 subst hpq,
696 intros,
697 refl },
st └┘
698 rw [Ap, Aq] at this,
699 -- deduce that the distances coincide up to `ε`, by a straightforward computation
700 -- that should be automated
701 have I := calc
702 abs (ε⁻¹) * abs (dist x y - dist (Ψ x) (Ψ y)) =
703 abs (ε⁻¹ * (dist x y - dist (Ψ x) (Ψ y))) : (abs_mul _ _).symm
id ┴
typ ┴
704 ... = abs ((ε⁻¹ * dist x y) - (ε⁻¹ * dist (Ψ x) (Ψ y))) : by { congr, ring }
st └┘
705 ... ≤ 1 : le_of_lt (abs_sub_lt_one_of_floor_eq_floor this),
706 calc
707 abs (dist x y - dist (Ψ x) (Ψ y)) = (ε * ε⁻¹) * abs (dist x y - dist (Ψ x) (Ψ y)) :
id ┴
typ ┴
708 by rw [mul_inv_cancel (ne_of_gt εpos), one_mul]
st ┴
709 ... = ε * (abs (ε⁻¹) * abs (dist x y - dist (Ψ x) (Ψ y))) :
710 by rw [abs_of_nonneg (le_of_lt (inv_pos εpos)), mul_assoc]
st ┴
711 ... ≤ ε * 1 : mul_le_mul_of_nonneg_left I (le_of_lt εpos)
712 ... = ε : mul_one _ } },
st └──┘
713 calc dist p q = GH_dist (p.rep) (q.rep) : dist_GH_dist p q
id └───┘ └───┘ ┴ ┴
src └───┘ └───┘
typ └───┘ └───┘ ┴ ┴
doc └───┘ └───┘
714 ... ≤ ε + ε/2 + ε : main
id ┴
typ ┴
715 ... = δ : by { simp [ε], ring }
id ┴ ┴
typ ┴ ┴
st └─
716 end
st ──┘
717
718 /-- Compactness criterion: a closed set of compact metric spaces is compact if the spaces have
719 a uniformly bounded diameter, and for all `ε` the number of balls of radius `ε` required
720 to cover the spaces is uniformly bounded. This is an equivalence, but we only prove the
721 interesting direction that these conditions imply compactness. -/
722 lemma totally_bounded {t : set GH_space} {C : ℝ} {u : ℕ → ℝ} {K : ℕ → ℕ}
id ┴ └──────┘ ┴ ┴ ┴ ┴ ┴
src ┴ └──────┘ ┴ ┴ ┴ ┴ ┴
typ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴
doc └──────┘
723 (ulim : tendsto u at_top (𝓝 0))
724 (hdiam : ∀p ∈ t, diam (univ : set (GH_space.rep p)) ≤ C)
id ┴ └┘ └┘ └┘ └┘ ┴ ┴
src └┘ └┘ └┘ └┘
typ ┴ └┘ └┘ └┘ └┘ ┴ ┴
doc └┘ └┘ └┘
725 (hcov : ∀p ∈ t, ∀n:ℕ, ∃s : set (GH_space.rep p), cardinal.mk s ≤ K n ∧ univ ⊆ ⋃x∈s, ball x (u n)) :
id ┴ ┴ └──┘ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └──┘ └──┘ ┴
typ ┴ ┴ └──┘ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘ └──┘
726 totally_bounded t :=
id ┴
typ ┴
727 begin
728 /- Let `δ>0`, and `ε = δ/5`. For each `p`, we construct a finite subset `s p` of `p`, which
729 is `ε`-dense and has cardinality at most `K n`. Encoding the mutual distances of points in `s p`,
730 up to `ε`, we will get a map `F` associating to `p` finitely many data, and making it possible to
731 reconstruct `p` up to `ε`. This is enough to prove total boundedness. -/
732 refine metric.totally_bounded_of_finite_discretization (λδ δpos, _),
id ┴
typ ┴
733 let ε := (1/5) * δ,
id ┴
typ ┴
734 have εpos : 0 < ε := mul_pos (by norm_num) δpos,
id ┴
typ ┴
735 -- choose `n` for which `u n < ε`
736 rcases metric.tendsto_at_top.1 ulim ε εpos with ⟨n, hn⟩,
id ┴
typ ┴
737 have u_le_ε : u n ≤ ε,
id ┴ ┴ ┴
typ ┴ ┴ ┴
738 { have := hn n (le_refl _),
id ┴
typ ┴
739 simp only [real.dist_eq, add_zero, sub_eq_add_neg, neg_zero] at this,
740 exact le_of_lt (lt_of_le_of_lt (le_abs_self _) this) },
st └┘
741 -- construct a finite subset `s p` of `p` which is `ε`-dense and has cardinal `≤ K n`
742 have : ∀p:GH_space, ∃s : set (p.rep), ∃N ≤ K n, ∃E : equiv s (fin N),
id └──────┘ └─┘ └──┘ ┴ ┴
src └──────┘ └─┘ └──┘
typ └──────┘ └─┘ └──┘ ┴ ┴
doc └──────┘ └──┘
743 p ∈ t → univ ⊆ ⋃x∈s, ball x (u n),
id ┴ └──┘ ┴ ┴ ┴
src └──┘
typ ┴ └──┘ ┴ ┴ ┴
744 { assume p,
745 by_cases hp : p ∉ t,
id ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴
746 { have : nonempty (equiv (∅ : set (p.rep)) (fin 0)),
id └──────┘ └───┘ └─┘ └───┘ └─┘
src └──────┘ └───┘ └─┘ └───┘ └─┘
typ └──────┘ └───┘ └─┘ └───┘ └─┘
doc └───┘ └───┘
747 { rw ← fintype.card_eq, simp },
st └┘
748 use [∅, 0, bot_le, choice (this)] },
st └┘
749 { rcases hcov _ (set.not_not_mem.1 hp) n with ⟨s, ⟨scard, scover⟩⟩,
id ┴
typ ┴
750 rcases cardinal.lt_omega.1 (lt_of_le_of_lt scard (cardinal.nat_lt_omega _)) with ⟨N, hN⟩,
751 rw [hN, cardinal.nat_cast_le] at scard,
752 have : cardinal.mk s = cardinal.mk (fin N), by rw [hN, cardinal.mk_fin],
id ┴ └─────────┘ └─┘ ┴
src └─────────┘ └─┘
typ ┴ └─────────┘ └─┘ ┴
doc └─────────┘
st ┴
753 cases quotient.exact this with E,
754 use [s, N, scard, E],
id ┴
typ ┴
755 simp [hp, scover] } },
st └──┘
756 choose s N hN E hs using this,
757 -- Define a function `F` taking values in a finite type and associating to `p` enough data
758 -- to reconstruct it up to `ε`, namely the (discretized) distances between elements of `s p`.
759 let M := (floor (ε⁻¹ * max C 0)).to_nat,
id ┴ ┴ └────┘
src └────┘
typ ┴ ┴ └────┘
760 let F : GH_space → (Σk:fin ((K n).succ), (fin k → fin k → fin (M.succ))) :=
id └──────┘ └─┘ ┴ ┴ └──┘ └────┘
src └──────┘ └──┘ └────┘
typ └──────┘ └─┘ ┴ ┴ └──┘ └────┘
doc └──────┘
761 λp, ⟨⟨N p, lt_of_le_of_lt (hN p) (nat.lt_succ_self _)⟩,
id ┴ ┴
typ ┴ ┴
762 λa b, ⟨min M (floor (ε⁻¹ * dist ((E p).inv_fun a) ((E p).inv_fun b))).to_nat,
id ┴ ┴ └────┘
src └────┘
typ ┴ ┴ └────┘
763 lt_of_le_of_lt ( min_le_left _ _) (nat.lt_succ_self _) ⟩ ⟩,
764 refine ⟨_, by apply_instance, (λp, F p), _⟩,
765 -- It remains to show that if `F p = F q`, then `p` and `q` are `ε`-close
766 rintros ⟨p, pt⟩ ⟨q, qt⟩ hpq,
767 have Npq : N p = N q := (fin.ext_iff _ _).1 (sigma.mk.inj_iff.1 hpq).1,
id ┴ ┴ ┴
typ ┴ ┴ ┴
768 let Ψ : s p → s q := λx, (E q).inv_fun (fin.cast Npq ((E p).to_fun x)),
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
769 let Φ : s p → q.rep := λx, Ψ x,
id ┴ └───┘
src └───┘
typ ┴ └───┘
doc └───┘
770 have main : GH_dist (p.rep) (q.rep) ≤ ε + ε/2 + ε,
id └───┘ └───┘ ┴
src └───┘ └───┘
typ └───┘ └───┘ ┴
doc └───┘ └───┘
771 { -- to prove the main inequality, argue that `s p` is `ε`-dense in `p`, and `s q` is `ε`-dense
772 -- in `q`, and `s p` and `s q` are almost isometric. Then closeness follows
773 -- from `GH_dist_le_of_approx_subsets`
774 refine GH_dist_le_of_approx_subsets Φ _ _ _,
775 show ∀x : p.rep, ∃ (y : p.rep) (H : y ∈ s p), dist x y ≤ ε,
id └───┘ ┴ ┴
src └───┘
typ └───┘ ┴ ┴
doc └───┘
776 { -- by construction, `s p` is `ε`-dense
777 assume x,
778 have : x ∈ ⋃y∈(s p), ball y (u n) := (hs p pt) (mem_univ _),
id ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
779 rcases mem_bUnion_iff.1 this with ⟨y, ys, hy⟩,
780 exact ⟨y, ys, le_trans (le_of_lt hy) u_le_ε⟩ },
id ┴ └────┘
typ ┴ └────┘
st └┘
781 show ∀x : q.rep, ∃ (z : s p), dist x (Φ z) ≤ ε,
id └───┘ ┴ ┴
src └───┘
typ └───┘ ┴ ┴
doc └───┘
782 { -- by construction, `s q` is `ε`-dense, and it is the range of `Φ`
783 assume x,
784 have : x ∈ ⋃y∈(s q), ball y (u n) := (hs q qt) (mem_univ _),
id ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
785 rcases mem_bUnion_iff.1 this with ⟨y, ys, hy⟩,
786 let i := ((E q).to_fun ⟨y, ys⟩).1,
id ┴ ┴
typ ┴ ┴
787 let hi := ((E q).to_fun ⟨y, ys⟩).2,
id ┴ ┴
typ ┴ ┴
788 have ihi_eq : (⟨i, hi⟩ : fin (N q)) = (E q).to_fun ⟨y, ys⟩, by rw fin.ext_iff,
id ┴ └─┘ ┴ ┴ ┴
src └─┘
typ ┴ └─┘ ┴ ┴ ┴
789 have hiq : i < N q := hi,
id ┴ ┴ ┴
typ ┴ ┴ ┴
790 have hip : i < N p, { rwa Npq.symm at hiq },
id ┴ ┴ ┴
typ ┴ ┴ ┴
st └┘
791 let z := (E p).inv_fun ⟨i, hip⟩,
id ┴ ┴ └─┘
typ ┴ ┴ └─┘
792 use z,
793 have C1 : (E p).to_fun z = ⟨i, hip⟩ := (E p).right_inv ⟨i, hip⟩,
id ┴ ┴ └─┘ ┴ ┴ └─┘
typ ┴ ┴ └─┘ ┴ ┴ └─┘
794 have C2 : fin.cast Npq ⟨i, hip⟩ = ⟨i, hi⟩ := rfl,
id └─┘ ┴
typ └─┘ ┴
795 have C3 : (E q).inv_fun ⟨i, hi⟩ = ⟨y, ys⟩, by { rw ihi_eq, exact (E q).left_inv ⟨y, ys⟩ },
id ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
st └┘
796 have : Φ z = y :=
id ┴
typ ┴
797 by { simp only [Φ, Ψ], rw [C1, C2, C3], refl },
st └┘
798 rw this,
799 exact le_trans (le_of_lt hy) u_le_ε },
id └────┘
typ └────┘
st └┘
800 show ∀x y : s p, abs (dist x y - dist (Φ x) (Φ y)) ≤ ε,
id ┴ ┴
typ ┴ ┴
801 { /- the distance between `x` and `y` is encoded in `F p`, and the distance between
802 `Φ x` and `Φ y` (two points of `s q`) is encoded in `F q`, all this up to `ε`.
803 As `F p = F q`, the distances are almost equal. -/
804 assume x y,
805 have : dist (Φ x) (Φ y) = dist (Ψ x) (Ψ y) := rfl,
806 rw this,
807 -- introduce `i`, that codes both `x` and `Φ x` in `fin (N p) = fin (N q)`
808 let i := ((E p).to_fun x).1,
id ┴
typ ┴
809 have hip : i < N p := ((E p).to_fun x).2,
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
810 have hiq : i < N q, by rwa Npq at hip,
id ┴ ┴ ┴
typ ┴ ┴ ┴
811 have i' : i = ((E q).to_fun (Ψ x)).1, by { simp [Ψ, (E q).right_inv _] },
id ┴ ┴ ┴
typ ┴ ┴ ┴
st └┘
812 -- introduce `j`, that codes both `y` and `Φ y` in `fin (N p) = fin (N q)`
813 let j := ((E p).to_fun y).1,
id ┴
typ ┴
814 have hjp : j < N p := ((E p).to_fun y).2,
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
815 have hjq : j < N q, by rwa Npq at hjp,
id ┴ ┴ ┴
typ ┴ ┴ ┴
816 have j' : j = ((E q).to_fun (Ψ y)).1, by { simp [Ψ, (E q).right_inv _] },
id ┴ ┴ ┴
typ ┴ ┴ ┴
st └┘
817 -- Express `dist x y` in terms of `F p`
818 have Ap : ((F p).2 ⟨i, hip⟩ ⟨j, hjp⟩).1 = (floor (ε⁻¹ * dist x y)).to_nat := calc
id ┴ ┴ └─┘ ┴ └─┘ ┴
typ ┴ ┴ └─┘ ┴ └─┘ ┴
819 ((F p).2 ⟨i, hip⟩ ⟨j, hjp⟩).1 = ((F p).2 ((E p).to_fun x) ((E p).to_fun y)).1 :
id ┴ ┴ ┴
typ ┴ ┴ ┴
820 by { congr; apply (fin.ext_iff _ _).2; refl }
st └┘
821 ... = min M (floor (ε⁻¹ * dist x y)).to_nat :
id ┴
typ ┴
822 by simp only [F, (E p).left_inv _]
id ┴
typ ┴
823 ... = (floor (ε⁻¹ * dist x y)).to_nat :
id ┴
typ ┴
824 begin
825 refine min_eq_right (int.to_nat_le_to_nat (floor_mono _)),
826 refine mul_le_mul_of_nonneg_left (le_trans _ (le_max_left _ _)) (le_of_lt (inv_pos εpos)),
827 change dist (x : p.rep) y ≤ C,
id └───┘ ┴
src └───┘
typ └───┘ ┴
doc └───┘
828 refine le_trans (dist_le_diam_of_mem compact_univ.bounded (mem_univ _) (mem_univ _)) _,
829 exact hdiam p pt
id ┴
typ ┴
830 end,
st └─┘
831 -- Express `dist (Φ x) (Φ y)` in terms of `F q`
832 have Aq : ((F q).2 ⟨i, hiq⟩ ⟨j, hjq⟩).1 = (floor (ε⁻¹ * dist (Ψ x) (Ψ y))).to_nat := calc
id ┴ ┴ └─┘ ┴ └─┘ ┴
typ ┴ ┴ └─┘ ┴ └─┘ ┴
833 ((F q).2 ⟨i, hiq⟩ ⟨j, hjq⟩).1 = ((F q).2 ((E q).to_fun (Ψ x)) ((E q).to_fun (Ψ y))).1 :
id ┴ ┴ ┴
typ ┴ ┴ ┴
834 by { congr; apply (fin.ext_iff _ _).2; [exact i', exact j'] }
st └┘
835 ... = min M (floor (ε⁻¹ * dist (Ψ x) (Ψ y))).to_nat :
id ┴
typ ┴
836 by simp only [F, (E q).left_inv _]
id ┴
typ ┴
837 ... = (floor (ε⁻¹ * dist (Ψ x) (Ψ y))).to_nat :
id ┴
typ ┴
838 begin
839 refine min_eq_right (int.to_nat_le_to_nat (floor_mono _)),
840 refine mul_le_mul_of_nonneg_left (le_trans _ (le_max_left _ _)) (le_of_lt (inv_pos εpos)),
841 change dist (Ψ x : q.rep) (Ψ y) ≤ C,
id └───┘ ┴
src └───┘
typ └───┘ ┴
doc └───┘
842 refine le_trans (dist_le_diam_of_mem compact_univ.bounded (mem_univ _) (mem_univ _)) _,
843 exact hdiam q qt
id ┴
typ ┴
844 end,
st └─┘
845 -- use the equality between `F p` and `F q` to deduce that the distances have equal
846 -- integer parts
847 have : ((F p).2 ⟨i, hip⟩ ⟨j, hjp⟩).1 = ((F q).2 ⟨i, hiq⟩ ⟨j, hjq⟩).1,
id ┴ └┘ └┘ ┴ ┴ └┘ ┴ └┘
typ ┴ └┘ └┘ ┴ ┴ └┘ ┴ └┘
848 { -- we want to `subst hpq` where `hpq : F p = F q`, except that `subst` only works
849 -- with a constant, so replace `F q` (and everything that depends on it) by a constant `f`
850 -- then `subst`
851 revert hiq hjq,
852 change N q with (F q).1,
id ┴ ┴ ┴
typ ┴ ┴ ┴
853 generalize_hyp : F q = f at hpq ⊢,
id ┴
typ ┴
854 subst hpq,
855 intros,
856 refl },
st └┘
857 have : floor (ε⁻¹ * dist x y) = floor (ε⁻¹ * dist (Ψ x) (Ψ y)),
id ┴
typ ┴
858 { rw [Ap, Aq] at this,
859 have D : 0 ≤ floor (ε⁻¹ * dist x y) :=
id ┴
typ ┴
860 floor_nonneg.2 (mul_nonneg (le_of_lt (inv_pos εpos)) dist_nonneg),
861 have D' : floor (ε⁻¹ * dist (Ψ x) (Ψ y)) ≥ 0 :=
id ┴
typ ┴
862 floor_nonneg.2 (mul_nonneg (le_of_lt (inv_pos εpos)) dist_nonneg),
863 rw [← int.to_nat_of_nonneg D, ← int.to_nat_of_nonneg D', this] },
st ┴ └┘
864 -- deduce that the distances coincide up to `ε`, by a straightforward computation
865 -- that should be automated
866 have I := calc
867 abs (ε⁻¹) * abs (dist x y - dist (Ψ x) (Ψ y)) =
868 abs (ε⁻¹ * (dist x y - dist (Ψ x) (Ψ y))) : (abs_mul _ _).symm
id ┴
typ ┴
869 ... = abs ((ε⁻¹ * dist x y) - (ε⁻¹ * dist (Ψ x) (Ψ y))) : by { congr, ring }
st └┘
870 ... ≤ 1 : le_of_lt (abs_sub_lt_one_of_floor_eq_floor this),
871 calc
872 abs (dist x y - dist (Ψ x) (Ψ y)) = (ε * ε⁻¹) * abs (dist x y - dist (Ψ x) (Ψ y)) :
id ┴
typ ┴
873 by rw [mul_inv_cancel (ne_of_gt εpos), one_mul]
st ┴
874 ... = ε * (abs (ε⁻¹) * abs (dist x y - dist (Ψ x) (Ψ y))) :
875 by rw [abs_of_nonneg (le_of_lt (inv_pos εpos)), mul_assoc]
st ┴
876 ... ≤ ε * 1 : mul_le_mul_of_nonneg_left I (le_of_lt εpos)
877 ... = ε : mul_one _ } },
st └──┘
878 calc dist p q = GH_dist (p.rep) (q.rep) : dist_GH_dist p q
id └───┘ └───┘ ┴ ┴
src └───┘ └───┘
typ └───┘ └───┘ ┴ ┴
doc └───┘ └───┘
879 ... ≤ ε + ε/2 + ε : main
id ┴
typ ┴
880 ... = δ/2 : by { simp [ε], ring }
id ┴
typ ┴
st └┘
881 ... < δ : half_lt_self δpos
id ┴
typ ┴
882 end
st └─┘
883
884 section complete
885
886 /- We will show that a sequence `u n` of compact metric spaces satisfying
887 `dist (u n) (u (n+1)) < 1/2^n` converges, which implies completeness of the Gromov-Hausdorff space.
888 We need to exhibit the limiting compact metric space. For this, start from
889 a sequence `X n` of representatives of `u n`, and glue in an optimal way `X n` to `X (n+1)`
890 for all `n`, in a common metric space. Formally, this is done as follows.
891 Start from `Y 0 = X 0`. Then, glue `X 0` to `X 1` in an optimal way, yielding a space
892 `Y 1` (with an embedding of `X 1`). Then, consider an optimal gluing of `X 1` and `X 2`, and
893 glue it to `Y 1` along their common subspace `X 1`. This gives a new space `Y 2`, with an
894 embedding of `X 2`. Go on, to obtain a sequence of spaces `Y n`. Let `Z0` be the inductive
895 limit of the `Y n`, and finally let `Z` be the completion of `Z0`.
896 The images `X2 n` of `X n` in `Z` are at Hausdorff distance `< 1/2^n` by construction, hence they
897 form a Cauchy sequence for the Hausdorff distance. By completeness (of `Z`, and therefore of its
898 set of nonempty compact subsets), they converge to a limit `L`. This is the nonempty
899 compact metric space we are looking for. -/
900
901 variables (X : ℕ → Type) [∀n, metric_space (X n)] [∀n, compact_space (X n)] [∀n, nonempty (X n)]
id ┴ ┴ └──────────┘ ┴ ┴ └───────────┘ ┴ ┴ └──────┘ ┴
src └──────────┘ └───────────┘ └──────┘
typ ┴ ┴ └──────────┘ ┴ ┴ └───────────┘ ┴ ┴ └──────┘ ┴
doc └──────────┘ └───────────┘
902
903 /-- Auxiliary structure used to glue metric spaces below, recording an isometric embedding
904 of a type `A` in another metric space. -/
905 structure aux_gluing_struct (A : Type) [metric_space A] : Type 1 :=
id └──┘ └──────────┘ ┴
src └──────────┘
typ └──┘ └──────────┘ ┴
doc └──────────┘
906 (space : Type)
id └──┘
typ └──┘
907 (metric : metric_space space)
id └──────────┘ └───┘
src └──────────┘
typ └──────────┘ └───┘
doc └──────────┘
908 (embed : A → space)
id ┴ ┴ └───┘
typ ┴ ┴ └───┘
909 (isom : isometry embed)
id └──────┘ └───┘
src └──────┘
typ └──────┘ └───┘
doc └──────┘
910
911 /-- Auxiliary sequence of metric spaces, containing copies of `X 0`, ..., `X n`, where each
912 `X i` is glued to `X (i+1)` in an optimal way. The space at step `n+1` is obtained from the space
913 at step `n` by adding `X (n+1)`, glued in an optimal way to the `X n` already sitting there. -/
914 def aux_gluing (n : ℕ) : aux_gluing_struct (X n) := nat.rec_on n
id ┴ └───────────────┘ ┴ ┴ └────────┘ ┴
src ┴ └───────────────┘ └────────┘
typ ┴ └───────────────┘ ┴ ┴ └────────┘ ┴
doc └───────────────┘
915 { space := X 0,
id ┴
typ ┴
916 metric := by apply_instance,
917 embed := id,
id └┘
src └┘
typ └┘
918 isom := λx y, rfl }
id ┴ ┴ └─┘
src └─┘
typ ┴ ┴ └─┘
919 (λn a, by letI : metric_space a.space := a.metric; exact
id ┴ ┴ └┘ └┘ └┘ └┘ └┘ └──┘ └┘ └┘ ┴
src └┘ └┘ └┘ └┘ └┘ └──┘ └┘ └┘ ┴
typ ┴ ┴ └┘ └┘ └┘ └┘ └┘ └──┘ └┘ └┘ ┴
doc └┘ └┘ └┘ └┘ ┴
920 { space := glue_space a.isom (isometry_optimal_GH_injl (X n) (X n.succ)),
id └─┘ └┘ └┘
src └─┘ └┘ └┘
typ └─┘ └┘ └┘
921 metric := metric.metric_space_glue_space a.isom (isometry_optimal_GH_injl (X n) (X n.succ)),
id └┘ └─┘ └─┘ └─┘ └─┘ └─┘ └─┘ └─┘
src └┘ └─┘ └─┘ └─┘ └─┘ └─┘ └─┘ └─┘
typ └┘ └─┘ └─┘ └─┘ └─┘ └─┘ └─┘ └─┘
922 embed := (to_glue_r a.isom (isometry_optimal_GH_injl (X n) (X n.succ)))
id └──┘ └─┘ └┘ └┘
src └──┘ └─┘ └┘ └┘
typ └──┘ └─┘ └┘ └┘
923 ∘ (optimal_GH_injr (X n) (X n.succ)),
id ┴ └┘ └┘ └┘ └┘
src ┴ └┘ └┘ └┘ └┘
typ ┴ └┘ └┘ └┘ └┘
doc └┘ └┘ └┘ └┘
924 isom := (to_glue_r_isometry _ _).comp (isometry_optimal_GH_injr (X n) (X n.succ)) })
id └┘ ┴ ┴ └────┘
src └┘ ┴ └────┘
typ └┘ ┴ ┴ └────┘
doc └┘ ┴
925
926 /-- The Gromov-Hausdorff space is complete. -/
927 instance : complete_space (GH_space) :=
id └────────────┘ └──────┘
src └────────────┘ └──────┘
typ └────────────┘ └──────┘
doc └────────────┘ └──────┘
928 begin
st └─────
929 have : ∀ (n : ℕ), 0 < ((1:ℝ) / 2) ^ n, by { apply _root_.pow_pos, norm_num },
id ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
st ─┘ └┘
930 -- start from a sequence of nonempty compact metric spaces within distance `1/2^n` of each other
931 refine metric.complete_of_convergent_controlled_sequences (λn, (1/2)^n) this (λu hu, _),
id ┴ └──┘ ┴
typ ┴ └──┘ ┴
932 -- `X n` is a representative of `u n`
933 let X := λn, (u n).rep,
id ┴ ┴ └─┘
src └─┘
typ ┴ ┴ └─┘
doc └─┘
934 -- glue them together successively in an optimal way, getting a sequence of metric spaces `Y n`
935 let Y := aux_gluing X,
id └────────┘ ┴
src └────────┘
typ └────────┘ ┴
doc └────────┘
936 letI : ∀n, metric_space (Y n).space := λn, (Y n).metric,
id ┴ └──────────┘ ┴ └───┘ ┴ ┴ └────┘
src └──────────┘ └───┘ └────┘
typ ┴ └──────────┘ ┴ └───┘ ┴ ┴ └────┘
doc └──────────┘
937 have E : ∀n:ℕ, glue_space (Y n).isom (isometry_optimal_GH_injl (X n) (X n.succ)) = (Y n.succ).space :=
id └────────┘ └──┘ ┴ └───┘ ┴ ┴ └───┘
src └────────┘ └──┘ └───┘ ┴ └───┘
typ └────────┘ └──┘ ┴ └───┘ ┴ ┴ └───┘
938 λn, by { simp [Y, aux_gluing], refl },
id ┴ ┴ └────────┘
src └────────┘
typ ┴ ┴ └────────┘
doc └────────┘
st └┘
939 let c := λn, cast (E n),
id ┴ └──┘
src └──┘
typ ┴ └──┘
940 have ic : ∀n, isometry (c n) := λn x y, rfl,
id ┴ ┴
typ ┴ ┴
941 -- there is a canonical embedding of `Y n` in `Y (n+1)`, by construction
942 let f : Πn, (Y n).space → (Y n.succ).space :=
id ┴ └───┘
src └───┘
typ ┴ └───┘
943 λn, (c n) ∘ (to_glue_l (aux_gluing X n).isom (isometry_optimal_GH_injl (X n) (X n.succ))),
id ┴ ┴
typ ┴ ┴
944 have I : ∀n, isometry (f n),
id ┴
typ ┴
945 { assume n,
946 apply isometry.comp,
947 { assume x y, refl },
st └┘
948 { apply to_glue_l_isometry } },
st └──┘
949 -- consider the inductive limit `Z0` of the `Y n`, and then its completion `Z`
950 let Z0 := metric.inductive_limit I,
951 let Z := uniform_space.completion Z0,
id └┘
typ └┘
952 let Φ := to_inductive_limit I,
953 let coeZ := (coe : Z0 → Z),
id └┘ ┴
typ └┘ ┴
954 -- let `X2 n` be the image of `X n` in the space `Z`
955 let X2 := λn, range (coeZ ∘ (Φ n) ∘ (Y n).embed),
id ┴ └──┘
typ ┴ └──┘
956 have isom : ∀n, isometry (coeZ ∘ (Φ n) ∘ (Y n).embed),
id ┴ └──┘
typ ┴ └──┘
957 { assume n,
958 apply isometry.comp completion.coe_isometry _,
959 apply isometry.comp _ (Y n).isom,
id ┴
typ ┴
960 apply to_inductive_limit_isometry },
st └┘
961 -- The Hausdorff distance of `X2 n` and `X2 (n+1)` is by construction the distance between
962 -- `u n` and `u (n+1)`, therefore bounded by `1/2^n`
963 have D2 : ∀n, Hausdorff_dist (X2 n) (X2 n.succ) < (1/2)^n,
id ┴
typ ┴
964 { assume n,
965 have X2n : X2 n = range ((coeZ ∘ (Φ n.succ) ∘ (c n)
id └┘ └──┘
typ └┘ └──┘
966 ∘ (to_glue_r (Y n).isom (isometry_optimal_GH_injl (X n) (X n.succ))))
967 ∘ (optimal_GH_injl (X n) (X n.succ))),
id └────┘
src └────┘
typ └────┘
968 { change X2 n = range (coeZ ∘ (Φ n.succ) ∘ (c n)
id └──┘
typ └──┘
969 ∘ (to_glue_r (Y n).isom (isometry_optimal_GH_injl (X n) (X n.succ)))
970 ∘ (optimal_GH_injl (X n) (X n.succ))),
id └────┘
src └────┘
typ └────┘
971 simp only [X2, Φ],
id └┘
typ └┘
972 rw [← to_inductive_limit_commute I],
973 simp only [f],
974 rw ← to_glue_commute },
st └┘
975 rw range_comp at X2n,
976 have X2nsucc : X2 n.succ = range ((coeZ ∘ (Φ n.succ) ∘ (c n)
id └┘ └──┘
typ └┘ └──┘
977 ∘ (to_glue_r (Y n).isom (isometry_optimal_GH_injl (X n) (X n.succ))))
978 ∘ (optimal_GH_injr (X n) (X n.succ))), by refl,
979 rw range_comp at X2nsucc,
980 rw [X2n, X2nsucc, Hausdorff_dist_image, Hausdorff_dist_optimal, ← dist_GH_dist],
981 { exact hu n n n.succ (le_refl n) (le_succ n) },
id └────┘ ┴
src └────┘
typ └────┘ ┴
st └┘
982 { apply isometry.comp completion.coe_isometry _,
983 apply isometry.comp _ ((ic n).comp (to_glue_r_isometry _ _)),
id ┴
typ ┴
984 apply to_inductive_limit_isometry } },
st └──┘
985 -- consider `X2 n` as a member `X3 n` of the type of nonempty compact subsets of `Z`, which
986 -- is a metric space
987 let X3 : ℕ → nonempty_compacts Z := λn, ⟨X2 n,
id ┴ ┴ └┘
typ ┴ ┴ └┘
988 ⟨range_nonempty _, compact_range (isom n).continuous ⟩⟩,
989 -- `X3 n` is a Cauchy sequence by construction, as the successive distances are
990 -- bounded by `(1/2)^n`
991 have : cauchy_seq X3,
992 { refine cauchy_seq_of_le_geometric (1/2) 1 (by norm_num) (λn, _),
id ┴
typ ┴
993 rw one_mul,
994 exact le_of_lt (D2 n) },
id ┴
typ ┴
st └┘
995 -- therefore, it converges to a limit `L`
996 rcases cauchy_seq_tendsto_of_complete this with ⟨L, hL⟩,
997 -- the images of `X3 n` in the Gromov-Hausdorff space converge to the image of `L`
998 have M : tendsto (λn, (X3 n).to_GH_space) at_top (𝓝 L.to_GH_space) :=
id ┴
typ ┴
999 tendsto.comp (to_GH_space_continuous.tendsto _) hL,
1000 -- By construction, the image of `X3 n` in the Gromov-Hausdorff space is `u n`.
1001 have : ∀n, (X3 n).to_GH_space = u n,
id ┴ ┴
typ ┴ ┴
1002 { assume n,
1003 rw [nonempty_compacts.to_GH_space, ← (u n).to_GH_space_rep,
id ┴ ┴
typ ┴ ┴
1004 to_GH_space_eq_to_GH_space_iff_isometric],
1005 constructor,
1006 convert (isom n).isometric_on_range.symm,
id ┴
typ ┴
1007 },
st └┘
1008 -- Finally, we have proved the convergence of `u n`
1009 exact ⟨L.to_GH_space, by simpa [this] using M⟩
1010 end
st └─┘
1011
1012 end complete--section
1013
1014 end Gromov_Hausdorff --namespace